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  pm2.43i 64  sylc 68  mtod 107  mt2d 110  mt3d 113  mt4d 114  mpbid 193  mpbird 194  jcai 287  mpan9 472  mpand 705  mp2and 707  mpdan 708  pclem6 746  ecase2d 756  mopick2 1476  euor2 1477  eqrdav 1517  sbcthdv 1992  sbciegf 2008  sseldd 2120  preq12b 2548  axpweq 2817  ordtri3or 3007  ordunidif 3022  ordtri2or2 3068  ordun 3071  suc11 3073  reuuni4 3110  reuuniss 3112  reuuniss2 3114  eldifpw 3133  onuni 3150  ordunel 3181  onsucuni2 3188  ordunisuc2 3198  limsssuc 3204  nnlim 3231  nnsuc 3235  peano5 3241  relop 3365  funopg 3652  fssxp 3744  fnbrfvb 3864  ssimaex 3879  ffvelrn 3928  dffo4 3934  fopab2 3937  fopabcos 3947  isofrlem 4015  oprabval6g 4093  elopabi 4179  eloprabi 4180  onfununi 4209  tz7.49 4260  oalimcl 4330  oaass 4331  omword2 4341  omlimcl 4345  odi 4346  oeworde 4356  nnarcl 4372  omsmolem 4396  mapvalg 4471  pmvalg 4472  mapsn 4486  f1imaen 4563  fundmen 4569  ac6sfi 4591  mapxpen 4642  omsdomnn 4676  pssnn 4681  ssnnfi 4682  ssfi 4683  unblem3 4688  unfi2 4698  unifi2 4702  fiint 4703  inf3lem5 4762  noinfep 4786  rankxplim3 4860  aceq5 4886  zorn2lem7 4940  fodom 4944  cardnn 4970  sucdom 4992  cardlim 5001  cardaleph 5035  nlt1pi 5187  indpi 5188  nsmallpq 5237  prnmadd 5254  genpnnp 5262  genpnmax 5264  prlem934b 5292  prlem934 5293  ltaddpr 5294  ltexprlem2 5297  ltexprlem7 5302  prlem936 5309  reclem2pr 5311  suppsr2 5377  suppsr3 5378  supsrlem2 5380  axrnegex 5437  cnegexlem1 5499  cnegexlem2 5500  cnegexlem3 5501  cnegex 5502  1re 5589  0re 5594  recex 5840  lep1 5952  letrp1 5956  lediv12a 6041  recreclt 6047  ledivp1 6050  nnrecgt0 6099  nndiv 6105  lbinfm 6216  bndndx 6241  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  supxrunb1 6257  elnnz1 6323  zltp1le 6349  zdiv 6356  zneo 6371  zindd 6386  btwnz 6387  uzwo3lem1 6388  qbtwnre 6418  qbtwnxr 6419  modabs2 6474  fsequb2 6655  uzrdgsuci 6668  seq1rn2 6686  seqzrn2 6751  expnlbnd2 6854  sqrlem12 6885  sqr2irr 6930  replim 6962  absor 7067  seq1ublem 7114  caubndi 7129  faclbnd 7148  facavg 7158  climconst3 7299  climaddlem3 7319  climmullem8 7330  climsqueeze 7343  climsqueeze2 7344  climcaui 7359  caucvglem6 7365  serzf0i 7372  ser1cmp2i 7380  isummulc1 7416  reccnv 7422  geoisumr 7448  cvgratlem1 7455  cvgratlem5 7459  ivthlem6 7491  ivthlem7 7492  efseq0ex 7516  eftlcl 7584  reeff1o 7634  sin02gt0 7687  absef 7692  infpnlem2 7719  infpn2 7721  infxpidmlem11 7774  infxpidmlem12 7775  infdif 7780  infdif2 7781  tgcl 7836  tgss2 7849  elcls3 7921  neii1 7931  neii2 7932  neiss 7933  neindisj 7941  tpnei 7944  neissex 7948  cnpco 7979  cncnplem4 7987  dnsconst 7998  metxplem4 8043  metxp 8044  ssblex 8066  opni3 8076  opnuni 8078  blopn 8086  metequiv 8091  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  lmuni 8162  lmle 8171  metelcls 8176  metcn4i 8183  xplmi 8184  xplm 8186  iscms2lem5 8204  cmsss 8208  bcthlem7 8216  bcthlem13 8222  bcthlem14 8223  bcthlem18 8227  bcthlem21 8230  bcthlem26 8235  bcthlem28 8237  bcthlem29 8238  bcthlem31 8240  bcthlem33 8242  grpidinvlem3 8263  grpidinv 8265  grpideu 8266  grprcan 8280  grpinveu 8281  isgrp2i 8293  grpasscan1 8294  gxneg 8322  gxsuc 8328  gxnn0add 8330  gxadd 8331  gxmul 8334  ring2 8391  vacnlem3 8584  vacnlem6 8587  nmblolbii 8714  blocnilem 8719  phpar2 8738  phpar 8739  siii 8769  ubthlem5 8791  ubthlem10 8796  minveclem25 8829  minveclem26 8830  minveclem27 8831  minvecex 8838  minveceu 8843  htthlem12 8893  pilem1 8938  pilem2 8939  sineq0 8983  sineq0OLD 8984  efifolem4 8997  shftefif1olem 9013  grothpw 9054  2bornot2b 9059  hlimcauii 9382  ocorth 9440  projlem25 9486  projlem26 9487  projlem31 9492  pjthlem11 9505  omlsii 9521  pjpj0i 9531  osumlem7 9862  spansncvi 9875  5oalem6 9882  unop 10119  hmop 10126  nmopun 10218  lnopconi 10242  lnfnconi 10269  nlelchi 10273  cnlnssadj 10292  rnbra 10320  cnvbraval 10323  leopmul 10347  nmopleid 10352  hmopidmchlem 10358  hmopidmchi 10359  hstel2 10427  stcltrlem2 10485  csmdsymi 10542  atsseq 10555  atcveq0 10556  hatomistici 10570  cvati 10574  atexch 10590  atomli 10591  atcvati 10595  irredlem2 10600  irredlem4 10602  irredi 10603  atmd 10608  mdsymlem3 10614  mdsymlem5 10616  sumdmdlem 10627  cdj3lem2b 10646  ghomid 10679  cayleylem2 10695  findreccl 10702  eloi 10817  exidu1 10902  rnplrnml0 10946  on1el3 10962  uznzr 10967  hmphre 11036  hmeogrp 11044  top2ind 11050  altretop 11144  trnij 11160  homib 11251  idfisf 11295  idsubfun 11312  ecase13d 11391  fiuni 11420  fictb 11423  finsschain 11425  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  onsdom 11437  omsubel 11444  omsublim 11448  infenomsub 11450  omsubinit 11451  cnpnei 11472  subcls 11481  subntr 11482  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  cncomp 11494  alexsublem4 11499  dfcon2 11501  connsub 11502  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem4 11510  reconnlem5 11511  reconn 11512  ivthALT 11515  1stcclb 11532  2ndcctbss 11539  fnetr 11556  reftr 11558  topfneec 11562  fnessref 11564  locfincomp 11575  locfincf 11577  neibastop2 11584  topmeet 11587  fnemeet1 11589  fnemeet2 11590  fbssint 11626  fbasfip 11627  fbunfip 11631  fgfil 11638  extbas1 11641  filrn 11643  filfinnfr 11646  filssufil 11656  uffinfix 11662  ufinffr 11663  ufilen 11664  ufcondr 11666  limfilcf 11683  cnpfillim 11686  fmfnfm 11704  fmufil 11705  flimfneii 11712  fcluscf 11724  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  dirref 11752  dirtr 11753  tailfb 11762  filnetlem3 11765  filnet 11768  isga 11772  dif1card 11835  findcard 11836  fimax 11837  fisupg 11839  indexf 11847  fipreima 11848  inficl 11849  frinfm 11850  fimaxre 11856  divexp 11859  uzp1 11863  fzm1 11867  absz 11868  rddif 11869  absrdbnd 11870  absmod0 11873  sdc 11877  incsequz2 11880  fsumlt 11884  fsumlt1 11894  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  hmeocnv 11959  haustlmu 11967  txcn 11979  txcnopab 11980  sstotbnd 11992  totbndss 11993  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem1 12011  heiborlem11 12021  heiborlem16 12026  heiborlem28 12038  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem36 12046  heiborlem37 12047  heiborlem40 12050  rrncms 12075

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

Copyright terms: Public domain