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 701  mp2and 703  mpdan 704  pclem6 741  ecase2d 751  mopick2 1436  euor2 1437  sbcthdv 1947  sbciegf 1960  sseldd 2068  preq12b 2483  reuuni4 2887  reuuniss 2889  reuuniss2 2891  eldifpw 2910  ordtri3or 2979  onuni 2996  ordunidif 3005  ordtri2or2 3078  ordun 3081  ordunel 3084  onsucuni2 3091  suc11 3093  ordunisuc2 3115  limsssuc 3121  nnlim 3144  nnsuc 3148  peano5 3153  relop 3275  funopg 3547  fssxp 3637  fnbrfvb 3753  ssimaex 3768  ffvelrn 3814  dffo4 3820  fopab2 3823  fopabcos 3833  isofrlem 3901  tz7.49 3959  oprabval6g 4032  elopabi 4117  eloprabi 4118  oalimcl 4194  oaass 4195  omword2 4205  omlimcl 4209  odi 4210  oeworde 4220  nnarcl 4232  omsmolem 4256  mapvalg 4330  pmvalg 4331  mapsn 4345  f1imaen 4421  fundmen 4427  mapxpen 4493  omsdomnn 4527  pssnn 4531  ssnnfi 4532  ssfi 4533  unblem3 4537  isfinite2 4541  unfi2 4547  unifi2 4551  fiint 4552  inf3lem5 4609  noinfep 4632  rankxplim3 4706  aceq5 4732  zorn2lem7 4786  fodom 4790  cardnn 4816  sucdom 4834  cardlim 4843  cardaleph 4877  nlt1pi 5025  indpi 5026  nsmallpq 5075  prnmadd 5092  genpnnp 5100  genpnmax 5102  prlem934b 5130  prlem934 5131  ltaddpr 5132  ltexprlem2 5135  ltexprlem7 5140  prlem936 5147  reclem2pr 5149  suppsr2 5215  suppsr3 5216  supsrlem2 5218  axrnegex 5275  cnegextlem1 5337  cnegextlem2 5338  cnegextlem3 5339  cnegext 5340  1re 5427  0re 5432  recext 5675  lep1t 5800  letrp1t 5804  lediv12it 5884  recrecltt 5890  ledivp1t 5893  nnrecgt0t 5941  nndivt 5947  lbinfm 6036  bndndx 6061  xrsupsslem 6064  xrinfmsslem 6065  xrsupss 6066  xrinfmss 6067  supxrunb1 6077  elnnz1 6143  zltp1let 6169  zneo 6188  btwnz 6203  uzwo3lem1 6204  qbtwnre 6264  qbtwnxr 6265  uzrdgsuc 6290  seq1rn2 6307  fsequb2 6510  seqzrn2 6542  sqrlem12 6670  sqr2irr 6715  replimt 6747  absort 6850  seq1ublem 6896  caubnd 6911  faclbnd 6930  facavgt 6940  climconst3 7081  climaddlem3 7101  climmullem8 7112  climsqueeze 7125  climsqueeze2 7126  climcau 7141  caucvglem6 7147  serzf0 7154  ser1f0 7155  ser1cmp2 7162  isummulc1 7197  reccnv 7203  geoisumr 7228  cvgratlem1 7235  cvgratlem5 7239  ivthlem6 7271  ivthlem7 7272  efseq0ex 7296  eftlclt 7364  reeff1o 7411  sin02gt0 7463  abseft 7468  infpnlem2 7492  infpn2 7494  infxpidmlem11 7547  infxpidmlem12 7548  infdif 7553  infdif2 7554  tgclt 7609  tgss2t 7622  fctop 7635  elcls3 7696  neii1 7706  neii2 7707  neiss 7708  neindisj 7716  tpnei 7719  neissex 7723  cnpco 7754  cncnplem4 7762  dnsconst 7773  metxplem4 7818  metxp 7819  ssblex 7841  opni3 7851  opnuni 7853  blopn 7861  metcnp 7872  metcnpi3 7877  metcnpi4 7878  metcni2 7880  lmuni 7936  lmle 7945  metelcls 7950  metcn4i 7957  xplmi 7958  xplm 7960  iscms2lem5 7978  cmsss 7982  bcthlem7 7990  bcthlem13 7996  bcthlem14 7997  bcthlem18 8001  bcthlem21 8004  bcthlem26 8009  bcthlem28 8011  bcthlem29 8012  bcthlem31 8014  bcthlem33 8016  grpidinvlem3 8035  grpidinv 8037  grpideu 8038  grprcan 8048  grpinveu 8049  isgrp2i 8061  grpasscan1 8062  ring2 8134  nmblolbii 8444  blocnilem 8449  phpar2 8467  phpar 8468  siii 8498  ubthlem5 8518  ubthlem10 8523  minveclem25 8554  minveclem26 8555  minveclem27 8556  minvecex 8563  minveceu 8568  htthlem12 8616  pilem1 8656  pilem2 8657  sineq0 8698  efifolem4 8710  shftefif1olem 8726  2bornot2b 8770  hlimcaui 9091  ocorth 9149  projlem25 9195  projlem26 9196  projlem31 9201  pjthlem11 9214  omlsi 9230  pjpj0 9240  osumlem7 9569  spansncv 9582  5oalem6 9589  unopt 9824  hmopt 9831  nmopunt 9924  lnopcon 9948  lnfncon 9975  nlelch 9979  cnlnssadj 9998  rnbra 10025  cnvbravalt 10028  leopmult 10052  nmopleidt 10057  hmopidmchlem 10063  hmopidmch 10064  hstel2t 10131  stcltrlem2 10189  csmdsym 10246  atsseq 10259  atcveq0 10260  hatomistic 10274  cvat 10278  atexcht 10293  atoml 10294  atcvat 10298  irredlem2 10303  irredlem4 10305  irred 10306  atmd 10311  mdsymlem3 10317  mdsymlem5 10319  sumdmdlem 10330  cdj3lem2b 10349  ghomid 10379  cayleylem2 10395  findreccl 10402  hmphre 10502  hmeogrp 10510  trnij 10580  eloi 10602  homib 10667  idfisf 10697

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

Copyright terms: Public domain