Theorem mpd 29

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 10	. 2 |- ((ph -> ps) -> (ph -> ch))
4	1, 3	ax-mp 7	1 |- (ph -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  syld 30  mpi 55  mpdd 57  mpcom 60  id 73  pm2.43i 78  sylc 82  syl3c 83  mtod 122  mt2d 125  mt3d 128  mt4d 129  mpbid 211  mpbird 212  jcai 311  mpan9OLD 520  mpand 762  mp2and 764  mpdan 765  pclem6 810  ecase2d 821  ee222 1115  mopick2OLD 1675  euor2OLD 1677  eqrdav 1720  sbcthdvOLD 2293  sbciegf 2316  sseldd 2453  tpid3g 2937  preq12b 2976  axpweq 3295  ordtri3or 3506  ordtri3orOLD 3507  ordunidif 3527  ordtri2or2 3579  ordun 3582  suc11 3584  reuuni4 3624  reuuniss 3626  reuuniss2 3628  euexeqOLD 3637  euexaleq 3638  eufromeq2 3640  eufromeq6 3644  eldifpw 3665  onuni 3685  ordunel 3717  onsucuni2OLD 3726  ordunisuc2 3737  limsssuc 3745  nnlim 3775  nnsuc 3780  peano5 3786  relop 3924  funopg 4265  fssxp 4386  fssxpOLD 4387  fnbrfvb 4523  fvelima 4534  ssimaex 4540  ffvelrn 4598  dffo4 4604  fopab2 4607  fopabcos 4617  isofrlem 4689  oprabval6g 4773  elopabi 4870  eloprabi 4871  reiotass2 4922  onfununi 4927  tz7.49 4979  oalimcl 5053  oaass 5054  omword2 5064  omlimcl 5068  odi 5069  oeworde 5079  nnarcl 5098  omsmolem 5124  mapvalg 5200  pmvalg 5201  mapsn 5215  f1imaen 5292  fundmen 5298  ac6sfi 5320  riota5 5390  mapxpen 5399  omsdomnn 5433  pssnn 5438  ssnnfi 5439  ssfi 5440  unblem3 5445  unfi2 5455  unifi2 5459  fiint 5460  ordiso 5493  ordtypelem6 5499  ordtypelem7 5500  onsdom 5504  inf3lem5 5532  noinfep 5556  rankxplim3 5634  cardnn 5666  omsubel 5679  omsublim 5683  infenomsub 5685  omsubinit 5686  aceq5 5698  zorn2lem7 5752  fodom 5756  sucdom 5790  cardlim 5799  cardaleph 5829  nlt1pi 5981  indpi 5982  nsmallpq 6031  prnmadd 6048  genpnnp 6056  genpnmax 6058  prlem934b 6086  prlem934 6087  ltaddpr 6088  ltexprlem2 6091  ltexprlem7 6096  prlem936 6103  reclem2pr 6105  suppsr2 6171  suppsr3 6172  supsrlem2 6174  axrnegex 6232  cnegexlem1 6295  cnegexlem2 6296  cnegexlem3 6297  cnegex 6298  1re 6394  0re 6399  recex 6672  lep1 6785  letrp1 6789  lediv12a 6874  recreclt 6880  ledivp1 6883  nnrecgt0 6932  nndiv 6938  lbinfm 7052  bndndx 7077  xrsupsslem 7080  xrinfmsslem 7081  xrsupss 7082  xrinfmss 7083  supxrunb1 7093  elnnz1 7159  zltp1le 7185  zdiv 7192  zneo 7207  zindd 7222  btwnz 7223  uzwo3lem1 7224  qbtwnre 7254  qbtwnxr 7255  modabs2 7310  fsequb2 7498  uzrdgsuci 7511  seq1rn2 7529  seqzrn2 7594  expnlbnd2 7698  sqrlem12 7729  sqr2irr 7774  replim 7806  absor 7911  seq1ublem 7958  caubndi 7973  faclbnd 7992  facavg 8002  hashginv 8026  climconst3 8151  climaddlem3 8171  climmullem8 8182  climsqueeze 8195  climsqueeze2 8196  climcaui 8211  caucvglem6 8217  serzf0i 8224  ser1cmp2i 8232  isummulc1 8268  reccnv 8274  geoisumr 8300  cvgratlem1 8307  cvgratlem5 8311  ivthlem6 8343  ivthlem7 8344  efseq0ex 8368  eftlcl 8436  reeff1o 8486  sin02gt0 8539  absef 8544  infpnlem2 8571  infpn2 8573  infxpidmlem11 8626  infxpidmlem12 8627  infdif 8632  infdif2 8633  tgcl 8689  tgss2 8702  fctop 8715  elcls3 8782  neii1 8792  neii2 8793  neiss 8794  neindisj 8802  tpnei 8805  neissex 8809  cnpnei 8838  cnpco 8841  cncnplem4 8849  dnsconst 8860  metxplem4 8905  metxp 8906  ssblex 8928  opni3 8938  opnuni 8940  blopn 8948  metequiv 8953  metcnp 8960  metcnpi3 8965  metcnpi4 8966  metcni2 8968  lmuni 9024  lmle 9033  metelcls 9038  metcn4i 9045  xplmi 9046  xplm 9048  iscms2lem5 9066  cmsss 9070  bcthlem7 9078  bcthlem13 9084  bcthlem14 9085  bcthlem18 9089  bcthlem21 9092  bcthlem26 9097  bcthlem28 9099  bcthlem29 9100  bcthlem31 9102  bcthlem33 9104  grpidinvlem3 9125  grpidinv 9127  grpideu 9128  grprcan 9142  grpinveu 9143  isgrp2i 9155  grpasscan1 9156  gxneg 9184  gxsuc 9190  gxnn0add 9192  gxadd 9193  gxmul 9196  isga 9245  ring2 9269  vacnlem3 9464  vacnlem6 9467  nmblolbii 9594  blocnilem 9599  phpar2 9618  phpar 9619  siii 9649  ubthlem5 9671  ubthlem10 9676  minveclem25 9709  minveclem26 9710  minveclem27 9711  minvecex 9718  minveceu 9723  htthlem12 9773  pilem1 9815  pilem2 9816  sineq0 9860  sineq0OLD 9861  efifolem4 9874  shftefif1olem 9890  grothpw 9929  2bornot2b 9938  dif1en 9966  dif1card 9969  findcard 9970  findcardOLD 9971  ghomid 9990  fiuni 10012  txcn 10019  txcnopab 10020  subtopmetlem 10047  subtopmet 10048  fbssint 10071  fbunfip 10074  fgfil 10082  extbas1 10083  filrn 10085  flimfneii 10112  cncomp 10123  dirref 10147  dirtr 10148  exidu1 10165  rnplrnml0 10194  on1el3 10204  uznzr 10208  hlimcauii 10531  ocorth 10589  projlem25 10635  projlem26 10636  projlem31 10641  pjthlem11 10654  omlsii 10670  pjpj0i 10680  osumlem7 11011  spansncvi 11024  5oalem6 11031  unop 11268  hmop 11275  nmopun 11368  lnopconi 11392  lnfnconi 11419  nlelchi 11423  cnlnssadj 11442  rnbra 11470  cnvbraval 11473  leopmul 11497  nmopleid 11502  opsqrlem1 11503  hmopidmchlem 11514  hmopidmchi 11515  hstel2 11583  stcltrlem2 11641  csmdsymi 11698  atsseq 11711  atcveq0 11712  hatomistici 11726  cvati 11730  atexch 11745  atomli 11746  atcvati 11750  irredlem2 11755  irredlem4 11757  irredi 11758  atmd 11763  mdsymlem3 11769  mdsymlem5 11771  sumdmdlem 11782  cdj3lem2b 11801  addltmulALT 11810  bnj1050 12681  bnj1072 12694  bnj1210 12777  bnj578 13083  bnj605 13084  bnj594 13092  bnj944 13132  bnj1128 13220  bnj1125 13222  bnj1145 13223  bnj1154 13230  bnj1388 13306  bnj1417 13322  fnn0ind 13403  cayleylem2 13434  dvds0 13462  absdvdsb 13465  dvdsabsb 13466  dvdsmul1 13468  dvdsleabs 13486  divalglem0 13488  divalglem9 13496  gcdcllem1 13510  gcdcllem3 13512  gcd0id 13521  gcdabs 13529  algcvga 13539  algfx 13540  eucalg 13547  mulgcdlem3 13550  mulgcdlem7 13554  isprm2lem 13566  coprm 13574  elres 13618  fundmpss 13629  dfon2lem3 13642  dfon2lem6 13645  dfon2lem8 13647  trcltr 13728  soxp 13742  frxp 13743  poseq 13746  wfrlem10 13758  sltval2 13789  axdenselem5 13813  axdenselem7 13815  axfelem10 13830  findreccl 13984  eloi 14130  fopab2g 14212  cbicplem 14234  supdef 14326  defgelem 14335  gaplc 14454  curgrpact 14458  grpdivone 14459  hmphre 14604  hmeogrp 14612  top2ind 14617  altretop 14707  cntrsetlem 14709  trnij 14725  lvsovso 14734  dualcat2lem 14811  homib 14827  idfisf 14871  idsubfun 14888  tarax3d2 14907  cptarc 14924  tarsuc2 14927  intartar 14937  carinttar2 14962  ecase13d 15032  fictb 15053  finsschain 15055  ordisoOLD 15056  ordtypelem6OLD 15062  ordtypelem7OLD 15063  onsdomOLD 15067  omsubelOLD 15074  omsublimOLD 15078  infenomsubOLD 15080  omsubinitOLD 15081  subcls 15106  subntr 15107  compsublem 15112  compsub 15113  cptclsscpt 15114  hscptsscld 15116  alexsublem4 15122  dfcon2 15124  connsub 15125  reconnlem1 15128  reconnlem4 15131  reconnlem5 15132  reconn 15133  ivthALT 15136  1stcclb 15153  2ndcctbss 15160  fnetr 15177  reftr 15179  topfneec 15183  fnessref 15185  locfincomp 15196  locfincf 15198  neibastop2 15205  topmeet 15208  fnemeet1 15210  fnemeet2 15211  fbasfip 15238  filfinnfr 15243  filssufil 15253  uffinfix 15259  ufinffr 15260  ufilen 15261  ufcondr 15263  limfilcf 15269  cnpfillim 15271  fmfnfm 15280  fmufil 15281  fcluscf 15294  fcluscnp 15300  fcluscomp 15303  ufcomp 15304  tailfb 15321  filnetlem3 15324  filnet 15327  unirep 15346  enf1f1o 15402  fimax 15428  fisupg 15430  indexfi 15437  fipreima 15438  inficl 15439  frinfm 15440  fisup2g 15450  fimax2g 15451  fimaxre 15456  fimaxre2 15457  divexp 15461  uzp1 15467  fzm1 15478  absz 15479  rddif 15480  absrdbnd 15481  absmod0 15484  sdc 15493  fdc 15494  fdc1 15495  incsequz2 15498  fsumlt 15503  fsumlt1 15513  blhalf 15528  mettrifi 15529  mettrifi2 15530  geomcau 15531  hmeocnv 15580  haustlmu 15588  cnresoprab 15597  sstotbnd 15618  totbndss 15619  totbndbnd 15626  ismtyhmeolem 15632  ismtybndlem 15634  heiborlem1 15637  heiborlem11 15647  heiborlem16 15652  heiborlem28 15664  heiborlem32 15668  heiborlem33 15669  heiborlem35 15671  heiborlem36 15672  heiborlem37 15673  heiborlem40 15676  rrncms 15701  ringneglmul 15786  ringnegrmul 15787  rngisocnv 15817  igenval 15891  isfldidl 15898  pridlc2 15902  pridlc3 15903  smoge 16136  ee333 16261  clatglble 16657  cmtbr4 16726  atomnle 16763  hlhght2 16780  hl0lt1 16781  hl1atom 16782  hlatmstc 16790  hl2atom 16794  cvr1 16795  cvrexchlem 16797  cvratlem 16799  cvrat 16800  cvrat3 16805  ps2 16808  grpidinvlem3NEW 16840  grpidinvNEW 16842  grpideuNEW 16843  grprcanNEW 16851  grpinveuNEW 16852  divrngidlemNEW 16894  paddasslem10 17002  paddasslem12 17004  paddasslem15 17007

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

Copyright terms: Public domain