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 472  mpand 703  mp2and 705  mpdan 706  pclem6 743  ecase2d 753  mopick2 1439  euor2 1440  sbcthdv 1950  sbciegf 1963  sseldd 2071  preq12b 2487  reuuni4 2893  reuuniss 2895  reuuniss2 2897  eldifpw 2916  ordtri3or 2985  onuni 3002  ordunidif 3011  ordtri2or2 3084  ordun 3087  ordunel 3090  onsucuni2 3097  suc11 3099  ordunisuc2 3121  limsssuc 3127  nnlim 3150  nnsuc 3154  peano5 3159  relop 3281  funopg 3553  fssxp 3643  fnbrfvb 3759  ssimaex 3774  ffvelrn 3820  dffo4 3826  fopab2 3829  fopabcos 3839  isofrlem 3907  tz7.49 3965  oprabval6g 4038  elopabi 4123  eloprabi 4124  oalimcl 4200  oaass 4201  omword2 4211  omlimcl 4215  odi 4216  oeworde 4226  nnarcl 4238  omsmolem 4262  mapvalg 4336  pmvalg 4337  mapsn 4351  f1imaen 4428  fundmen 4434  mapxpen 4501  omsdomnn 4538  pssnn 4544  ssnnfi 4545  ssnnfiOLD 4546  ssfi 4547  ssfiOLD 4548  unblem3 4553  isfinite2OLD 4558  unfi2 4565  unfi2OLD 4566  unifi2OLD 4571  fiint 4572  fiintOLD 4573  inf3lem5 4626  noinfep 4650  rankxplim3 4724  aceq5 4750  zorn2lem7 4804  fodom 4808  cardnn 4834  sucdom 4852  sucdomOLD 4853  cardlim 4862  cardaleph 4896  nlt1pi 5045  indpi 5046  nsmallpq 5095  prnmadd 5112  genpnnp 5120  genpnmax 5122  prlem934b 5150  prlem934 5151  ltaddpr 5152  ltexprlem2 5155  ltexprlem7 5160  prlem936 5167  reclem2pr 5169  suppsr2 5235  suppsr3 5236  supsrlem2 5238  axrnegex 5295  cnegextlem1 5357  cnegextlem2 5358  cnegextlem3 5359  cnegext 5360  1re 5447  0re 5452  recext 5696  lep1t 5814  letrp1t 5818  lediv12it 5898  recrecltt 5904  ledivp1t 5907  nnrecgt0t 5955  nndivt 5961  lbinfm 6050  bndndx 6075  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  supxrunb1 6091  elnnz1 6157  zltp1let 6183  zneo 6202  btwnz 6217  uzwo3lem1 6218  qbtwnre 6279  qbtwnxr 6280  uzrdgsuc 6305  seq1rn2 6322  fsequb2 6525  seqzrn2 6557  sqrlem12 6685  sqr2irr 6730  replimt 6762  absort 6865  seq1ublem 6911  caubnd 6926  faclbnd 6945  facavgt 6955  climconst3 7096  climaddlem3 7116  climmullem8 7127  climsqueeze 7140  climsqueeze2 7141  climcau 7156  caucvglem6 7162  serzf0 7169  ser1f0 7170  ser1cmp2 7177  isummulc1 7212  reccnv 7218  geoisumr 7243  cvgratlem1 7250  cvgratlem5 7254  ivthlem6 7286  ivthlem7 7287  efseq0ex 7311  eftlclt 7379  reeff1o 7426  sin02gt0 7479  abseft 7484  infpnlem2 7508  infpn2 7510  infxpidmlem11 7563  infxpidmlem12 7564  infdif 7569  infdif2 7570  tgclt 7623  tgss2t 7636  fctopOLD 7647  elcls3 7708  neii1 7718  neii2 7719  neiss 7720  neindisj 7728  tpnei 7731  neissex 7735  cnpco 7766  cncnplem4 7774  dnsconst 7785  metxplem4 7830  metxp 7831  ssblex 7853  opni3 7863  opnuni 7865  blopn 7873  metcnp 7884  metcnpi3 7889  metcnpi4 7890  metcni2 7892  lmuni 7948  lmle 7957  metelcls 7962  metcn4i 7969  xplmi 7970  xplm 7972  iscms2lem5 7990  cmsss 7994  bcthlem7 8002  bcthlem13 8008  bcthlem14 8009  bcthlem18 8013  bcthlem21 8016  bcthlem26 8021  bcthlem28 8023  bcthlem29 8024  bcthlem31 8026  bcthlem33 8028  grpidinvlem3 8047  grpidinv 8049  grpideu 8050  grprcan 8059  grpinveu 8060  isgrp2i 8072  grpasscan1 8073  ring2 8145  nmblolbii 8455  blocnilem 8460  phpar2 8478  phpar 8479  siii 8509  ubthlem5 8529  ubthlem10 8534  minveclem25 8565  minveclem26 8566  minveclem27 8567  minvecex 8574  minveceu 8579  htthlem12 8627  pilem1 8666  pilem2 8667  sineq0 8708  efifolem4 8720  shftefif1olem 8736  2bornot2b 8780  hlimcaui 9101  ocorth 9159  projlem25 9205  projlem26 9206  projlem31 9211  pjthlem11 9224  omlsi 9240  pjpj0 9250  osumlem7 9579  spansncv 9592  5oalem6 9599  unopt 9834  hmopt 9841  nmopunt 9934  lnopcon 9958  lnfncon 9985  nlelch 9989  cnlnssadj 10008  rnbra 10035  cnvbravalt 10038  leopmult 10062  nmopleidt 10067  hmopidmchlem 10073  hmopidmch 10074  hstel2t 10141  stcltrlem2 10199  csmdsym 10256  atsseq 10269  atcveq0 10270  hatomistic 10284  cvat 10288  atexcht 10303  atoml 10304  atcvat 10308  irredlem2 10313  irredlem4 10315  irred 10316  atmd 10321  mdsymlem3 10327  mdsymlem5 10329  sumdmdlem 10340  cdj3lem2b 10359  ghomid 10389  cayleylem2 10405  findreccl 10412  hmphre 10516  hmeogrp 10524  top2ind 10534  trnij 10608  eloi 10630  homib 10695  idfisf 10731

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

Copyright terms: Public domain