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 698  mp2and 700  mpdan 701  pclem6 738  ecase2d 748  mopick2 1413  euor2 1414  sbcthdv 1918  sbciegf 1931  sseldd 2039  preq12b 2453  reuuni4 2850  reuuniss 2852  reuuniss2 2854  eldifpw 2873  ordtri3or 2942  onuni 2959  ordunidif 2968  ordtri2or2 3041  ordun 3044  ordunel 3047  onsucuni2 3054  suc11 3056  ordunisuc2 3078  limsssuc 3084  nnlim 3107  nnsuc 3111  peano5 3116  fssxp 3576  fnbrfvb 3692  ssimaex 3707  ffvelrn 3753  dffo4 3759  fopab2 3762  fopabcos 3772  isofrlem 3840  tz7.49 3898  oprabval6g 3971  elopabi 4055  eloprabi 4056  oalimcl 4132  oaass 4133  omword2 4143  omlimcl 4147  odi 4148  oeworde 4158  nnarcl 4170  omsmolem 4194  mapvalg 4268  pmvalg 4269  mapsn 4283  f1imaen 4357  fundmen 4363  mapxpen 4427  omsdomnn 4461  pssnn 4465  ssnn 4466  ssfi 4467  unblem3 4471  isfinite2 4475  unfilem3 4478  unfi2 4481  unifi2 4485  fiint 4486  inf3lem5 4541  noinfep 4564  rankxplim3 4638  aceq5 4664  zorn2lem7 4718  fodom 4722  cardnn 4748  sucdom 4765  cardlim 4774  cardaleph 4808  nlt1pi 4956  indpi 4957  nsmallpq 5006  prnmadd 5023  genpnnp 5031  genpnmax 5033  prlem934b 5061  prlem934 5062  ltaddpr 5063  ltexprlem2 5066  ltexprlem7 5071  prlem936 5078  reclem2pr 5080  suppsr2 5146  suppsr3 5147  supsrlem2 5149  axrnegex 5206  cnegextlem1 5268  cnegextlem2 5269  cnegextlem3 5270  cnegext 5271  1re 5358  0re 5363  recext 5608  lep1t 5719  letrp1t 5723  lediv12it 5795  recrecltt 5801  ledivp1t 5804  nnrecgt0t 5851  nndivt 5857  lbinfm 5946  bndndx 5971  xrsupsslem 5974  xrinfmsslem 5975  xrsupss 5976  xrinfmss 5977  supxrunb1 5987  elnnz1 6053  zltp1let 6079  zneo 6098  btwnz 6114  uzwo3lem1 6115  qbtwnre 6167  qbtwnxr 6168  uzrdgsuc 6192  seq1rn2 6209  fsequb2 6407  seqzrn2 6439  sqrlem12 6565  sqr2irr 6610  replimt 6643  absort 6751  seq1ublem 6799  caubnd 6814  faclbnd 6833  facavgt 6843  climconst3 6984  climaddlem3 7003  climmullem8 7014  climsqueeze 7027  climsqueeze2 7028  climcau 7043  caucvglem6 7049  serzf0 7056  ser1f0 7057  ser1cmp2 7064  isummulc1 7098  reccnv 7104  geoisumr 7129  cvgratlem1 7136  cvgratlem5 7140  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  efseq0ex 7204  eftlclt 7272  reeff1o 7319  sin02gt0 7371  abseft 7376  infpnlem2 7401  infpn2 7403  infxpidmlem11 7456  infxpidmlem12 7457  infdif 7462  infdif2 7463  tgclt 7517  tgss2t 7530  fctop 7543  elcls3 7600  neii1 7610  neii2 7611  neiss 7612  neindisj 7620  tpnei 7623  neissex 7627  cnpco 7656  cncnplem4 7664  dnsconst 7675  metxplem4 7721  metxp 7722  ssblex 7744  opni3 7754  opnuni 7756  blopn 7764  metcnp 7774  metcnpi3 7779  metcnpi4 7780  metcni2 7782  lmuni 7834  lmle 7843  metelcls 7848  metcn4i 7854  xplmi 7855  xplm 7857  iscms2lem5 7875  cmsss 7879  bcthlem7 7887  bcthlem13 7893  bcthlem14 7894  bcthlem18 7898  bcthlem21 7901  bcthlem26 7906  bcthlem28 7908  bcthlem29 7909  bcthlem31 7911  bcthlem33 7913  grpidinvlem3 7932  grpidinv 7934  grpideu 7935  grprcan 7945  grpinveu 7946  grpasscan1OLD 7956  isgrp2i 7959  grpasscan1 7960  ring2 8034  nmblolbii 8325  blocnilem 8330  phpar2 8348  phpar 8349  siii 8379  ubthlem5 8399  ubthlem10 8404  minveclem25 8435  minveclem26 8436  minveclem27 8437  minvecex 8444  minveceu 8449  htthlem12 8495  pilem1 8503  pilem2 8504  efifolem4 8553  shftefif1olem 8574  shftefif1olemOLD 8575  ghomid 8661  cayleylem2 8677  findreccl 8684  hmphre 8768  hmeogrp 8776  trnij 8831  eloi 8853  homib 8918  2bornot2b 8965  hlimcaui 9257  ocorth 9294  projlem25 9340  projlem26 9341  projlem31 9346  pjthlem11 9358  omlsi 9374  pjpj0 9384  osumlem7 9715  spansncv 9728  5oalem6 9735  unopt 9969  hmopt 9976  nmopunt 10068  lnopcon 10092  lnfncon 10119  nlelch 10123  cnlnssadj 10142  rnbra 10167  cnvbravalt 10170  leopmult 10193  nmopleidt 10197  hmopidmchlem 10203  hmopidmch 10204  hstel2t 10270  strlem6 10307  hstrlem6 10315  stcltrlem2 10328  csmdsym 10383  atsseq 10396  atcveq0 10397  hatomistic 10411  cvat 10415  atexcht 10430  atoml 10431  atcvat 10435  irredlem2 10440  irredlem4 10442  irred 10443  atmd 10448  mdsymlem3 10454  mdsymlem5 10456  sumdmdlem 10466  cdj3lem2b 10483

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

Copyright terms: Public domain