HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem mpan 693
Description: An inference based on modus ponens.
Hypotheses
Ref Expression
mpan.1 |- ph
mpan.2 |- ((ph /\ ps) -> ch)
Assertion
Ref Expression
mpan |- (ps -> ch)
Proof of Theorem mpan
StepHypRef Expression
1 mpan.1 . 2 |- ph
2 mpan.2 . . 3 |- ((ph /\ ps) -> ch)
32ex 373 . 2 |- (ph -> (ps -> ch))
41, 3ax-mp 7 1 |- (ps -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  mp2an 695  mpanl1 704  mpanl12 706  mp3an1 900  mp3an12 903  mp3an13 904  sbcbii 1968  sbcel12g 2001  sbceqdig 2002  csbie2t 2023  csbnestg 2026  csbabg 2033  ssdifss 2158  elssuni 2516  difexg 2712  rabexg 2714  unipw 2746  sspwuni 2748  unexb 2864  difex2 2867  opeluu 2869  uniexb 2897  fr2nr 2915  fr3nr 2916  onminsb 2999  onminesb 3000  onintrab 3003  onnminsb 3006  onminex 3010  onel 3088  onuninsuc 3098  limuni3 3113  on0eqelt 3114  dfom2 3123  tfindsg2 3153  brrelexi 3198  relsn 3244  xpexg 3249  opabid2 3257  dmexg 3344  rnexg 3345  resiexg 3380  imaexg 3400  soirri 3428  sotri 3429  dfrel2 3471  coi1 3496  cnvexg 3505  coexg 3510  resfunexg 3565  cofunexg 3566  opabex2g 3597  fssxp 3622  fssres 3628  fcoi1 3630  fcoi2 3631  fabexg 3638  f1oabexg 3685  fvopab3 3762  fvimacnv 3790  ffvelrni 3800  rnssopab 3810  fopabco 3817  fopabcos 3818  fvconst2 3831  rdgsucopab 3931  rdglim2 3934  frsucopab 3939  tz7.48lem 3940  tz7.48-1 3941  tz7.48-2 3942  tz7.49 3944  tz7.49c 3945  abianfplem 3946  abianfp 3947  oprabex2g 4005  oprabval 4008  ndmopr 4031  1stcof 4085  elopabi 4101  eloprabi 4102  ordgt0ge1 4128  oe0m 4141  oa0r 4157  om0r 4158  om1r 4161  oe1m 4163  oawordeulem 4172  oaass 4179  odi 4194  omass 4195  oneo 4196  oen0 4197  oewordi 4202  oewordri 4203  oaabslem 4235  oaabs 4236  mapex 4312  map0 4328  ixpexg 4342  f1oen 4379  ssdomg 4389  snfi 4413  undom 4418  xpdom3 4425  mapdom2 4474  pwen 4483  limenpsi 4485  limensuci 4486  php 4493  onomeneq 4498  0sdom1dom 4504  omsdomnn 4509  domfi 4516  unblem4 4520  unfilem1 4524  unifi 4532  pwfi 4545  supmo 4550  suppr 4562  supsnALT 4564  inf0 4578  infensuc 4610  r1tr 4626  r1ord 4627  tz9.12lem1 4631  tz9.12lem3 4633  tz9.12 4634  rankon 4643  rankr1lem 4645  rankval3 4653  bndrank 4654  unbndrank 4655  rankr1b 4671  rankval4 4674  rankbnd2 4676  rankxplim 4684  rankxplim3 4686  rankxpsuc 4687  scott0 4689  karden 4698  numth2 4757  numthcor 4758  zorn2lem2 4761  zorn2lem4 4763  zorn2lem5 4764  zorn 4769  brdom7disj 4776  brdom6disj 4777  iundom 4784  oncardval 4791  oncardon 4792  oncardid 4793  oncard 4801  cardne 4802  carden 4803  sucdom 4814  unxpdom2 4817  sucxpdom 4818  cardidm 4821  cardsdomel 4824  carduni 4830  cardmin 4832  cardprc 4833  alephon 4837  alephcard 4839  alephordi 4846  alephgeom 4854  alephprc 4865  alephfplem3 4870  alephfp 4872  cardcf 4883  cfsuc 4887  cdaun 4894  cdadom2 4906  indpi 5006  ltsopq 5047  ltrpq 5057  prub 5070  genpnnp 5080  distrlem4pr 5102  prlem934b 5110  ltapr 5123  addcanpr 5124  suplem2pr 5134  ltsosr 5175  sqgt0sr 5187  mappsrpr 5190  suppsr2 5195  suppsr3 5196  supsrlem1 5197  ltsor 5233  axmulopr 5238  axmulass 5250  axdistr 5251  axcnre 5258  pre-axlttri 5259  pre-axlttrn 5260  addid2t 5301  cnegextlem2 5318  cnegext 5320  0cnALT 5322  addcan 5323  negclt 5340  mulid2t 5389  muladd11t 5394  mul02t 5416  mulm1t 5443  axmulgt0 5478  lttri2t 5485  lttri3t 5486  ltnrt 5503  mnfltt 5516  pnfnltt 5519  mnflet 5522  xrlttri2t 5528  xrlttri3t 5529  xrltnet 5538  ngtmnftt 5540  ne0gt0t 5593  lt0neg2t 5642  le0neg2t 5644  recextlem1 5655  recext 5657  mulcan 5659  mul0or 5663  divassz 5708  divdiv23z 5750  ltp1t 5767  lemul1it 5793  lemul1itOLD 5794  recgt0 5816  ltdiv23 5842  recp1lt1 5849  recrecltt 5850  posex 5856  squeeze0 5872  nnleltp1t 5901  nnsub 5903  nnaddm1clt 5905  avglet 5991  suprubi 6009  suprleubi 6012  xrsupsslem 6023  xrinfmsslem 6024  nn0ge0t 6064  nn0ltp1let 6074  elnn0z 6094  elnnz1 6102  elnn0nn 6118  zltp1let 6128  recnzt 6138  zneo 6147  zneoOLD 6148  zqt 6198  nnrecqt 6214  qbtwnxr 6217  qsqueeze 6218  rpge0t 6225  om2uzuz 6234  om2uzran 6237  uzrdgsuc 6241  seq1m1 6256  seq1rn2 6258  shftfval 6279  shftidt 6292  icounlem 6345  snunioolem 6347  uzind4i 6386  fzelp1 6441  fzshftralt 6454  fseqsupub 6458  seq1seq02t 6475  seqz1 6479  seqzp1 6480  seq0p1 6483  seqzval2t 6485  1expt 6516  0expt 6521  expge0t 6522  expge1t 6524  expwordit 6534  exple1t 6538  expubndt 6539  sqgt0 6558  sqlecant 6572  subsq2t 6574  bernneq 6583  bernneq2 6584  expnbndt 6585  discrlem2 6587  nnesq 6592  sqrlem5 6607  sqrlem6 6608  sqrlem12 6614  sqrlem16 6618  sqrlem17 6619  sqrge0 6632  sqrmsq 6639  crrecz 6672  rimul 6675  replimtOLD 6693  crret 6702  crimt 6704  imret 6710  reim0t 6711  recjt 6753  imcjt 6754  cjreimt 6763  cjreim2t 6764  cj11t 6765  absreimsqt 6791  absreimt 6792  absdivz 6794  absort 6800  absnid 6806  abslt 6810  absle 6811  absltOLD 6812  absleOLD 6813  cjdiv 6826  abs3lem 6838  abs1m 6841  cau5i 6854  cvg3 6860  caubnd 6863  facdivt 6879  faclbnd2 6883  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd5 6890  bcnp11t 6903  bcnp1nt 6904  bcpasc 6907  bccl2t 6909  sumex 6919  fsum1slem 6946  fsum1s 6947  csbfsumlem 6964  serzsplit 6994  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem5 7008  binomlem6 7009  binom1p 7011  clm2 7016  clm4 7018  clm0 7021  clm0nns 7023  climconst 7031  climunii 7035  climreu 7038  climshft 7041  climshft2 7043  iserzshft2 7044  climrecl 7047  climge0 7049  climaddlem2 7051  climaddc2 7055  climmullem1 7056  climmullem2 7057  climmullem3 7058  climmullem4 7059  climmullem7 7062  climsub 7066  clim2serzt 7070  clim2serz 7081  iserzex 7082  climubi 7089  climsup 7091  climcau 7092  caucvglem6 7098  caucvg 7099  caucvg3a 7100  caucvg3lem 7102  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1cmp2 7113  cvgcmp2lem 7116  cvgcmp2clem 7118  isumshft 7139  isumshft2 7140  isumclt 7144  iserzgt0 7146  reccnv 7153  infcvglem1 7156  infcvglem3 7158  expcnvlem2 7163  expcnvlem6 7167  geoser 7169  geolimilem 7170  geolim1i 7173  geoisum 7177  geoisum1 7179  geoisum1c 7180  0.999... 7181  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  cncfval 7199  ivthlem1 7216  ivthlem2 7217  ivthlem7 7222  ivthlem7OLD 7231  efcltlem1 7246  dfef2 7249  ef0lem 7252  efclt 7254  efcvg 7256  efcvgfsum 7257  reefcl 7259  erelem1 7261  erelem2 7262  erelem3 7263  efcj 7278  efaddlem1 7280  efaddlem2 7281  efaddlem3 7282  efaddlem5 7284  efaddlem6 7285  efaddlem10 7289  efaddlem11 7290  efaddlem13 7292  efaddlem16 7295  efaddlem17 7296  efaddlem19 7298  efaddlem25 7304  efaddlem26 7305  efaddlem27 7306  efsubt 7313  efnn0valt 7315  eftabs 7317  eftlexOLD 7319  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  absef01tllem 7328  eirrlem2 7331  eirrlem3 7332  eirrlem4 7333  eirrlem5 7334  abspef01tlub 7336  efsep 7337  effsumle 7338  efm1lim 7351  absefm1le 7352  eflegeolem1 7353  eflegeolem2 7354  efcnlem1 7359  reeff1o 7368  sinclt 7373  cosclt 7374  resinvalt 7375  recosvalt 7376  efi4pt 7377  resin4pt 7378  recos4pt 7379  resinclt 7380  recosclt 7381  sinnegt 7384  cosnegt 7385  efivalt 7389  efmivalt 7390  efeult 7391  sin01bndlem1 7409  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  cos01gt0 7419  sin02gt0 7420  demoivre 7426  demoivreALT 7427  acdc3lem 7428  acdclem 7436  nn0ennn 7439  znnenlem 7443  znnenlemOLD 7444  znnen 7445  unbenlem 7447  ruclem13 7465  ruclem15 7467  ruclem28 7480  ruclem31 7483  infxpidmlem10 7504  infxpidmlem12 7506  infunabs 7508  infcdaabs 7509  infcda 7510  infdif 7511  infdif2 7512  infxp 7515  infmap1 7516  iunctb 7517  unctb 7519  infmap2 7523  alephadd 7524  alephexp1 7526  alephexp2 7528  gch-kn 7529  tgvalt 7558  metgt0 7761  metxplem3 7768  metxp 7774  blfval 7775  bl2in 7783  lpbl 7819  lmfval 7863  caufval 7864  lmbr 7866  lmnn 7873  iscau 7874  lmclim 7898  metelcls 7900  xplm 7909  oprcn 7911  opr1scn 7914  bopcnlem1 7915  bopcnlem4 7918  cncms 7932  bcthlem1 7933  bcthlem7 7939  bcthlem8 7940  bcthlem9 7941  bcthlem10 7942  bcthlem11 7943  bcthlem16 7948  bcthlem18 7950  bcthlem20 7952  bcthlem21 7953  bcthlem22 7954  bcthlem23 7955  bcthlem28 7960  bcthlem33 7965  isgrp2i 8011  issubgi 8059  addinv 8065  ablmul 8068  mulid 8069  ghgrpilem1 8070  ghgrpilem3 8072  ghgrpilem4 8073  ghgrpi 8074  isvc 8138  nvop2 8165  nvvop 8166  nvop 8244  cnnvdemo 8248  imsmetlem 8261  sqcn 8270  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  ipfval 8286  ipval2 8291  4ipval2 8292  4ipval3 8296  ipid 8297  ipcl 8299  ipcj 8301  ip1cnilem1 8307  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem4 8310  ip1cnilem5 8311  ip1cnilem6 8312  sspival 8331  lnocoi 8352  nmoubi 8367  nmoub3i 8368  nmounbi 8371  0oo 8381  nmlno0lem 8385  nmlnogt0 8389  nmblolbii 8390  blocnilem 8395  blocni 8396  phop 8408  cnph 8409  ipasslem1 8421  ipasslem2 8422  ipasslem4 8424  ipasslem5 8425  ipasslem9 8429  ipasslem11 8431  siilem1 8442  siii 8444  ipblnfi 8447  ip2eqi 8448  ubthlem4 8463  ubthlem5 8464  ubthlem6 8465  ubthlem7 8466  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  minveclem5 8480  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem16 8491  minveclem18 8493  minveclem19 8494  minveclem20 8495  minveclem21 8496  minveclem22 8497  minveclem25 8500  minveclem26 8501  minveclem27 8502  minveclem28 8503  minveclem29 8504  minveclem30 8505  minveclem31 8506  minveclem35 8510  minveclem36 8511  minveclem37 8512  minveclem38 8513  minveceu 8514  htthlem6 8555  htthlem7 8556  htthlem8 8557  htthlem9 8558  htthlem10 8559  htthlem12 8561  sincolem 8584  sincnlem 8585  pilem1 8590  pilem2 8591  pilem3 8592  sinperlem1 8605  efimpi 8615  sinhalfpip 8616  sinhalfpim 8617  coshalfpip 8618  coshalfpim 8619  sincosq1sgn 8621  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  sincos6thpi 8628  cosh111lem1 8629  efghgrpilem 8634  efif 8636  efifolem1 8637  efifolem2 8638  efifolem4 8640  efifolem6 8642  efif1lem1 8645  efif1lem4 8648  efielcircOLD 8655  circgrpOLD 8658  efielcirc 8659  shftefif1olem 8661  shftefif1olemOLD 8662  eff1lem 8664  eff1i 8665  effoi 8666  effoiOLD 8667  efper 8669  eflogt 8682  logeft 8684  logcltOLD 8703  eflogtOLD 8704  logeftOLD 8705  hvsubopr 8806  hvsubclt 8808  hv2negt 8818  hvaddsubvalt 8823  hvsub4t 8827  hvaddsub12t 8828  hvpncant 8829  hvaddsubasst 8831  hvsubdistr1t 8837  hvaddeq0t 8857  hvsubcant 8862  his2subt 8879  hi01t 8883  normnegt 8932  norm3lem 8937  hilabl 8948  hilid 8949  hilnorm 8951  hhcms 8993  hhssnv 9054  hhsscms 9067  projlem6 9107  projlem26 9127  pjthlem2 9135  pjthlem3 9136  pjthlem7 9140  pjthlem8 9141  pjtheu 9150  omlsi 9160  pjcl 9166  pjhcl 9167  ococint 9212  spanvalt 9214  spanclt 9219  shlub 9261  shslub 9273  h1de2ctlem 9394  spanunsn 9419  pjoml6 9449  cm0t 9469  osumlem7 9501  spansncv 9514  pjocin 9560  pjin 9561  pjjs 9562  pjrn 9564  pjv 9567  pjds 9574  pjoi0 9580  mayete3 9590  ho0valt 9593  homulid2t 9643  hosubnegt 9650  hosubdit 9651  honegsubdit 9653  honegsubdi2t 9654  hosub4t 9656  hoaddsubasst 9658  hosubsub4t 9661  eigre 9677  eigpos 9679  nmopsetretHIL 9708  adjvalt 9731  adjt 9773  nmlnop0ALT 9835  lnopeq0 9847  hmopdt 9862  nmbdoplb 9864  nmcopexlem3 9868  nmcopexlem4 9869  nmcoplb 9873  lnopcon 9878  nmbdfnlb 9893  nmcfnexlem3 9897  nmcfnexlem4 9898  nmcfnlb 9902  lnfncon 9905  nlelsh 9908  nlelch 9909  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem7 9921  adjbd1o 9933  nmopadjle 9936  nmopadjlem 9937  nmopco 9942  nmopcoadj 9948  branmfnt 9951  bra11 9954  cnvbravalt 9956  cnvbraclt 9957  cnvbrabrat 9958  bracnvbrat 9959  leoppost 9971  nmopleidt 9983  pjnmop 9986  hmopidmchlem 9989  pjss1co 10002  pjnormss 10007  pjorthco 10008  pjtot 10017  pjadj3t 10025  pjinvar 10029  pjclem4a 10036  pj3lem1 10044  pj3s 10045  pjs14 10048  hst1ht 10064  strlem4 10091  strlem5 10092  hstrlem4 10099  hstrlem5 10100  jplem1 10105  mdslle1 10152  mdslle2 10153  mdslj1 10154  mdslj2 10155  mdsl1 10156  mdsl2 10157  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd2 10165  csmdsym 10169  mdexch 10170  elat2 10175  shatomic 10193  shatomistic 10196  chrelat 10199  chrelat2 10200  cvat 10201  cvbr3 10202  cvexchlem 10203  atoml 10217  atoml2 10218  atord 10219  atcvat2 10222  irredlem4 10228  atcvat3 10231  atcvat4 10232  atabs 10236  mdsymlem1 10238  mdsymlem3 10240  mdsymlem5 10242  mdsymlem6 10243  sumdmdlem 10252  sumdmdlem2 10253  dmdbr5at 10255  cdj1 10265  cdj3lem1 10266  ghomgrpilem2 10291  symggrpiOLD 10311  symggrpi 10313  cayleylem1 10316  cayleylem2 10317  cayleylem3 10318  uninqs 10342  qusp 10430  efilcp 10445  efilcp2 10450  mslb1 10473  2wsms 10474  eloi 10503  dedalg 10520  catded 10541  hgrablkcard 10610
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain