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

Step	Hyp	Ref	Expression
1		mpd.1	. 2 |- (ph -> ps)
2		mpd.2	. . 3 |- (ph -> (ps -> ch))
3	2	a2i 9	. 2 |- ((ph -> ps) -> (ph -> ch))
4	1, 3	ax-mp 7	1 |- (ph -> ch)

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 700  mp2and 702  mpdan 703  pclem6 740  ecase2d 750  mopick2 1434  euor2 1435  sbcthdv 1943  sbciegf 1956  sseldd 2064  preq12b 2479  reuuni4 2882  reuuniss 2884  reuuniss2 2886  eldifpw 2905  ordtri3or 2974  onuni 2991  ordunidif 3000  ordtri2or2 3073  ordun 3076  ordunel 3079  onsucuni2 3086  suc11 3088  ordunisuc2 3110  limsssuc 3116  nnlim 3139  nnsuc 3143  peano5 3148  relop 3270  funopg 3539  fssxp 3628  fnbrfvb 3744  ssimaex 3759  ffvelrn 3805  dffo4 3811  fopab2 3814  fopabcos 3824  isofrlem 3892  tz7.49 3950  oprabval6g 4023  elopabi 4107  eloprabi 4108  oalimcl 4184  oaass 4185  omword2 4195  omlimcl 4199  odi 4200  oeworde 4210  nnarcl 4222  omsmolem 4246  mapvalg 4320  pmvalg 4321  mapsn 4335  f1imaen 4409  fundmen 4415  mapxpen 4481  omsdomnn 4515  pssnn 4519  ssnn 4520  ssfi 4521  unblem3 4525  isfinite2 4529  unfi2 4535  unifi2 4539  fiint 4540  inf3lem5 4597  noinfep 4620  rankxplim3 4694  aceq5 4720  zorn2lem7 4774  fodom 4778  cardnn 4804  sucdom 4822  cardlim 4831  cardaleph 4865  nlt1pi 5013  indpi 5014  nsmallpq 5063  prnmadd 5080  genpnnp 5088  genpnmax 5090  prlem934b 5118  prlem934 5119  ltaddpr 5120  ltexprlem2 5123  ltexprlem7 5128  prlem936 5135  reclem2pr 5137  suppsr2 5203  suppsr3 5204  supsrlem2 5206  axrnegex 5263  cnegextlem1 5325  cnegextlem2 5326  cnegextlem3 5327  cnegext 5328  1re 5415  0re 5420  recext 5665  lep1t 5776  letrp1t 5780  lediv12it 5852  recrecltt 5858  ledivp1t 5861  nnrecgt0t 5908  nndivt 5914  lbinfm 6003  bndndx 6028  xrsupsslem 6031  xrinfmsslem 6032  xrsupss 6033  xrinfmss 6034  supxrunb1 6044  elnnz1 6110  zltp1let 6136  zneo 6155  btwnz 6171  uzwo3lem1 6172  qbtwnre 6224  qbtwnxr 6225  uzrdgsuc 6249  seq1rn2 6266  fsequb2 6464  seqzrn2 6496  sqrlem12 6622  sqr2irr 6667  replimt 6700  absort 6808  seq1ublem 6856  caubnd 6871  faclbnd 6890  facavgt 6900  climconst3 7041  climaddlem3 7060  climmullem8 7071  climsqueeze 7084  climsqueeze2 7085  climcau 7100  caucvglem6 7106  serzf0 7113  ser1f0 7114  ser1cmp2 7121  isummulc1 7155  reccnv 7161  geoisumr 7186  cvgratlem1 7193  cvgratlem5 7197  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  efseq0ex 7261  eftlclt 7329  reeff1o 7376  sin02gt0 7428  abseft 7433  infpnlem2 7458  infpn2 7460  infxpidmlem11 7513  infxpidmlem12 7514  infdif 7519  infdif2 7520  tgclt 7574  tgss2t 7587  fctop 7600  elcls3 7661  neii1 7671  neii2 7672  neiss 7673  neindisj 7681  tpnei 7684  neissex 7688  cnpco 7719  cncnplem4 7727  dnsconst 7738  metxplem4 7785  metxp 7786  ssblex 7808  opni3 7818  opnuni 7820  blopn 7828  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcni2 7847  lmuni 7902  lmle 7911  metelcls 7916  metcn4i 7922  xplmi 7923  xplm 7925  iscms2lem5 7943  cmsss 7947  bcthlem7 7955  bcthlem13 7961  bcthlem14 7962  bcthlem18 7966  bcthlem21 7969  bcthlem26 7974  bcthlem28 7976  bcthlem29 7977  bcthlem31 7979  bcthlem33 7981  grpidinvlem3 8000  grpidinv 8002  grpideu 8003  grprcan 8013  grpinveu 8014  isgrp2i 8026  grpasscan1 8027  ring2 8101  nmblolbii 8403  blocnilem 8408  phpar2 8426  phpar 8427  siii 8457  ubthlem5 8477  ubthlem10 8482  minveclem25 8513  minveclem26 8514  minveclem27 8515  minvecex 8522  minveceu 8527  htthlem12 8574  pilem1 8609  pilem2 8610  efifolem4 8659  shftefif1olem 8680  2bornot2b 8724  hlimcaui 9045  ocorth 9103  projlem25 9149  projlem26 9150  projlem31 9155  pjthlem11 9167  omlsi 9183  pjpj0 9193  osumlem7 9524  spansncv 9537  5oalem6 9544  unopt 9778  hmopt 9785  nmopunt 9877  lnopcon 9901  lnfncon 9928  nlelch 9932  cnlnssadj 9951  rnbra 9978  cnvbravalt 9981  leopmult 10005  nmopleidt 10010  hmopidmchlem 10016  hmopidmch 10017  hstel2t 10084  strlem6 10121  hstrlem6 10129  stcltrlem2 10142  csmdsym 10198  atsseq 10211  atcveq0 10212  hatomistic 10226  cvat 10230  atexcht 10245  atoml 10246  atcvat 10250  irredlem2 10255  irredlem4 10257  irred 10258  atmd 10263  mdsymlem3 10269  mdsymlem5 10271  sumdmdlem 10281  cdj3lem2b 10298  ghomid 10328  cayleylem2 10344  findreccl 10351  hmphre 10453  hmeogrp 10461  trnij 10517  eloi 10539  homib 10604

This theorem was proved from axioms:  ax-2 5  ax-mp 7

Copyright terms: Public domain