HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem mpd 26
Description: A modus ponens deduction.
Hypotheses
Ref Expression
mpd.1 |- (ph -> ps)
mpd.2 |- (ph -> (ps -> ch))
Assertion
Ref Expression
mpd |- (ph -> ch)
Proof of Theorem mpd
StepHypRef Expression
1 mpd.1 . 2 |- (ph -> ps)
2 mpd.2 . . 3 |- (ph -> (ps -> ch))
32a2i 9 . 2 |- ((ph -> ps) -> (ph -> ch))
41, 3ax-mp 7 1 |- (ph -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  syld 27  mpi 44  mpdd 46  mpcom 49  id 59  sylc 68  mtod 108  mt2d 111  mt3d 114  mt4d 115  mpbid 195  mpbird 196  jcai 289  mpan9 470  mpand 699  mp2and 701  mpdan 702  pclem6 739  ecase2d 749  mopick2 1429  euor2 1430  sbcthdv 1937  sbciegf 1950  sseldd 2058  preq12b 2474  reuuni4 2877  reuuniss 2879  reuuniss2 2881  eldifpw 2900  ordtri3or 2969  onuni 2986  ordunidif 2995  ordtri2or2 3068  ordun 3071  ordunel 3074  onsucuni2 3081  suc11 3083  ordunisuc2 3105  limsssuc 3111  nnlim 3134  nnsuc 3138  peano5 3143  relop 3265  funopg 3533  fssxp 3622  fnbrfvb 3738  ssimaex 3753  ffvelrn 3799  dffo4 3805  fopab2 3808  fopabcos 3818  isofrlem 3886  tz7.49 3944  oprabval6g 4017  elopabi 4101  eloprabi 4102  oalimcl 4178  oaass 4179  omword2 4189  omlimcl 4193  odi 4194  oeworde 4204  nnarcl 4216  omsmolem 4240  mapvalg 4314  pmvalg 4315  mapsn 4329  f1imaen 4403  fundmen 4409  mapxpen 4475  omsdomnn 4509  pssnn 4513  ssnn 4514  ssfi 4515  unblem3 4519  isfinite2 4523  unfilem3 4526  unfi2 4529  unifi2 4533  fiint 4534  inf3lem5 4589  noinfep 4612  rankxplim3 4686  aceq5 4712  zorn2lem7 4766  fodom 4770  cardnn 4796  sucdom 4814  cardlim 4823  cardaleph 4857  nlt1pi 5005  indpi 5006  nsmallpq 5055  prnmadd 5072  genpnnp 5080  genpnmax 5082  prlem934b 5110  prlem934 5111  ltaddpr 5112  ltexprlem2 5115  ltexprlem7 5120  prlem936 5127  reclem2pr 5129  suppsr2 5195  suppsr3 5196  supsrlem2 5198  axrnegex 5255  cnegextlem1 5317  cnegextlem2 5318  cnegextlem3 5319  cnegext 5320  1re 5407  0re 5412  recext 5657  lep1t 5768  letrp1t 5772  lediv12it 5844  recrecltt 5850  ledivp1t 5853  nnrecgt0t 5900  nndivt 5906  lbinfm 5995  bndndx 6020  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  supxrunb1 6036  elnnz1 6102  zltp1let 6128  zneo 6147  btwnz 6163  uzwo3lem1 6164  qbtwnre 6216  qbtwnxr 6217  uzrdgsuc 6241  seq1rn2 6258  fsequb2 6456  seqzrn2 6488  sqrlem12 6614  sqr2irr 6659  replimt 6692  absort 6800  seq1ublem 6848  caubnd 6863  faclbnd 6882  facavgt 6892  climconst3 7033  climaddlem3 7052  climmullem8 7063  climsqueeze 7076  climsqueeze2 7077  climcau 7092  caucvglem6 7098  serzf0 7105  ser1f0 7106  ser1cmp2 7113  isummulc1 7147  reccnv 7153  geoisumr 7178  cvgratlem1 7185  cvgratlem5 7189  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efseq0ex 7253  eftlclt 7321  reeff1o 7368  sin02gt0 7420  abseft 7425  infpnlem2 7450  infpn2 7452  infxpidmlem11 7505  infxpidmlem12 7506  infdif 7511  infdif2 7512  tgclt 7566  tgss2t 7579  fctop 7592  elcls3 7652  neii1 7662  neii2 7663  neiss 7664  neindisj 7672  tpnei 7675  neissex 7679  cnpco 7708  cncnplem4 7716  dnsconst 7727  metxplem4 7773  metxp 7774  ssblex 7796  opni3 7806  opnuni 7808  blopn 7816  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  lmuni 7886  lmle 7895  metelcls 7900  metcn4i 7906  xplmi 7907  xplm 7909  iscms2lem5 7927  cmsss 7931  bcthlem7 7939  bcthlem13 7945  bcthlem14 7946  bcthlem18 7950  bcthlem21 7953  bcthlem26 7958  bcthlem28 7960  bcthlem29 7961  bcthlem31 7963  bcthlem33 7965  grpidinvlem3 7984  grpidinv 7986  grpideu 7987  grprcan 7997  grpinveu 7998  grpasscan1OLD 8008  isgrp2i 8011  grpasscan1 8012  ring2 8086  nmblolbii 8390  blocnilem 8395  phpar2 8413  phpar 8414  siii 8444  ubthlem5 8464  ubthlem10 8469  minveclem25 8500  minveclem26 8501  minveclem27 8502  minvecex 8509  minveceu 8514  htthlem12 8561  pilem1 8590  pilem2 8591  efifolem4 8640  shftefif1olem 8661  shftefif1olemOLD 8662  2bornot2b 8724  hlimcaui 9027  ocorth 9080  projlem25 9126  projlem26 9127  projlem31 9132  pjthlem11 9144  omlsi 9160  pjpj0 9170  osumlem7 9501  spansncv 9514  5oalem6 9521  unopt 9755  hmopt 9762  nmopunt 9854  lnopcon 9878  lnfncon 9905  nlelch 9909  cnlnssadj 9928  rnbra 9953  cnvbravalt 9956  leopmult 9979  nmopleidt 9983  hmopidmchlem 9989  hmopidmch 9990  hstel2t 10056  strlem6 10093  hstrlem6 10101  stcltrlem2 10114  csmdsym 10169  atsseq 10182  atcveq0 10183  hatomistic 10197  cvat 10201  atexcht 10216  atoml 10217  atcvat 10221  irredlem2 10226  irredlem4 10228  irred 10229  atmd 10234  mdsymlem3 10240  mdsymlem5 10242  sumdmdlem 10252  cdj3lem2b 10269  ghomid 10299  cayleylem2 10317  findreccl 10324  hmphre 10417  hmeogrp 10425  trnij 10481  eloi 10503  homib 10568
This theorem was proved from axioms:  ax-2 5  ax-mp 7
Copyright terms: Public domain