Theorem mpd 11

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:  syl 13  id 15  mpdd 20  syldOLD 34  sylc 44  sylcOLD 45  mpi 97  mpcom 101  pm2.43i 108  syl3c 111  mtod 152  mt2d 156  mt3d 160  mt4d 163  mpbid 317  mpbird 318  jcai 500  mpdanOLD 674  mpandOLD 685  mp2and 691  pclem6OLD 1053  ecase2d 1065  ecase2dOLD 1066  ee1111 1573  eqrdav 2140  vtoclgft 2671  sbciegf 2722  sseldd 2851  tpid3g 3310  preq12b 3341  axpweq 3648  ordtri3or 3843  ordunidif 3858  ordtri2or2 3908  ordun 3911  suc11 3913  reuuni4 3951  reuuniss 3953  reuuniss2 3955  eusv2OLD 3963  eusv2 3964  reusv2lem2 3968  reusv6OLD 3977  eldifpw 4000  onuni 4017  ordunel 4048  ordunisuc2 4065  limsssuc 4071  nnlim 4099  nnsuc 4103  peano5 4109  relop 4242  elres 4368  funopg 4556  fssxp 4669  fnbrfvbg 4797  fvelima 4809  ssimaex 4814  fvopab4t 4825  ffvelrn 4877  dffo4 4883  fopab2 4888  fopabcos 4898  isofrlem 4974  f1oiso2 4978  oprabval6g 5056  elopabi 5172  eloprabi 5173  soxp 5213  fnwelem 5215  reiotass2 5246  onfununi 5253  smoge 5281  tz7.49OLD 5333  oalimcl 5405  oaass 5406  omword2 5416  omlimcl 5420  odi 5421  omeulem1 5424  omeu 5426  oeworde 5434  nnarcl 5450  omsmolem 5474  mapvalg 5550  pmvalg 5551  mapsn 5565  f1imaen 5642  fundmen 5648  omxpenlem 5669  ac6sfi 5675  riota5f 5754  riotasvd 5758  riotasv3d 5765  mapxpen 5780  infensuc 5793  sucdom2 5810  omsdomnn 5826  fineqvlem 5829  pssnn 5834  ssnnfi 5835  ssfi 5836  dif1en 5842  findcard 5843  fimax 5846  fisupg 5848  fimax2g 5849  unblem3 5854  unfi2 5865  unifi2 5871  fiint 5872  indexfi 5878  fipreima 5879  fisup2g 5908  ordiso 5914  ordtypelem6 5920  ordtypelem7 5921  onsdom 5925  inf3lem5 5955  noinfep 5983  rankxplim3 6061  onfrALT 6083  cardnnOLD 6119  carden2a 6121  carddomi2 6125  cardlim 6127  cardsdomelir 6128  cardsdomel2 6129  cardprclem 6134  cardmin2 6138  cardsucinf 6140  dif1cardOLD 6144  infxpenlem 6147  omsubel 6174  omsublim 6178  infenomsub 6180  omsubinit 6181  aceq5 6194  fodomnumlem 6208  cardaleph 6214  cdainflem 6257  onacda 6259  nnaun 6262  cff1 6278  cfflb 6279  cofsmo 6284  cfsmolem 6285  cfidm 6290  alephsing 6291  axcc3 6295  domtriomlem 6296  domtriomlemOLD 6298  axdc3lem2 6306  axdc3lem4 6308  axdc4lem 6310  axcclem 6312  zorn2lem7 6367  fodom 6374  sucdomOLD 6409  cardlimOLD 6417  konigthlem 6429  cardalephOLD 6443  pwcfsdom 6450  nlt1pi 6551  indpi 6552  nsmallpq 6601  prnmadd 6618  genpnnp 6626  genpnmax 6628  prlem934b 6656  prlem934 6657  ltaddpr 6658  ltexprlem2 6661  ltexprlem7 6666  prlem936 6673  reclem2pr 6675  suppsr2 6741  suppsr3 6742  supsrlem2 6744  axrnegex 6799  1re 6839  00id 6970  mul02lem1 6971  addid1 6977  cnegex 6979  addid2 6981  recex 7208  lep1 7321  letrp1 7325  lediv12a 7412  recreclt 7418  nnrecgt0 7470  nndiv 7476  lbinfm 7597  bndndx 7622  xrsupsslem 7625  xrinfmsslem 7626  xrsupss 7627  xrinfmss 7628  supxrunb1 7638  elnnz1 7705  zltp1le 7732  zdiv 7740  zneo 7755  fnn0ind 7769  zindd 7772  btwnz 7773  uzwo3lem1 7774  qbtwnre 7805  qbtwnxr 7806  modabs2 7861  fsequb2 8074  uzrdgsuci 8087  seq1rn2 8107  seqzrn2 8178  expnlbnd2 8287  sqrlem12 8318  sqr2irr 8363  replim 8395  absor 8500  seq1ublem 8548  caubndi 8563  faclbnd 8582  facavg 8592  hashginv 8617  hashginvOLD 8619  hashen 8621  hashenOLD 8623  fseq1hash 8629  climconst3 8752  climaddlem3 8772  climmullem8 8783  climsqueeze 8796  climsqueeze2 8797  climcaui 8812  caucvglem6 8818  serzf0i 8825  ser1cmp2i 8833  isummulc1 8869  reccnv 8875  supcvglem 8876  geoisumr 8903  cvgratlem1 8910  cvgratlem5 8914  ivthlem6 8946  ivthlem7 8947  efseq0ex 8971  eftlcl 9039  reeff1o 9089  sin02gt0 9142  absef 9147  infxpidmlem11OLD 9225  infxpidmlem12OLD 9226  infdif 9231  infdif2 9232  dvds0 9259  absdvdsb 9262  dvdsabsb 9263  dvdsmul1 9265  dvdsleabs 9287  divalglem0 9290  divalglem9 9298  gcdcllem1 9312  gcdcllem3 9314  gcd0id 9323  gcdabs 9331  algcvga 9342  algfx 9343  eucalg 9350  mulgcdlem3 9353  mulgcdlem7 9357  isprm2lem 9368  coprm 9377  prmdvdsexpb 9384  infpnlem2 9389  infpn2 9391  prmunb 9392  1arithlem14 9407  1arithlem15 9408  1arithlem16 9409  1arithlem23 9417  1arithlem24 9418  1arithlem31 9425  grpidinvlem3 9475  grpidinv 9477  grpideu 9478  grprcan 9487  grpinveu 9488  divrngidlem 9530  clatglble 9684  tgcl 9745  tgss2 9758  fctop 9771  elcls3 9851  neii1 9862  neii2 9863  neiss 9864  neindisj 9872  tpnei 9876  neissex 9880  cnpnei 9909  cnpco 9912  cncnplem4 9920  dnsconst 9931  metxplem4 9976  metxp 9977  ssblex 9999  opni3 10009  opnuni 10011  blopn 10019  metequiv 10024  metcnp 10031  metcnpi3 10036  metcnpi4 10037  metcni2 10039  lmuni 10095  lmle 10104  metelcls 10109  metcn4i 10116  xplmi 10117  xplm 10119  iscms2lem5 10137  cmsss 10141  bcthlem7 10149  bcthlem13 10155  bcthlem14 10156  bcthlem18 10160  bcthlem21 10163  bcthlem26 10168  bcthlem28 10170  bcthlem29 10171  bcthlem31 10173  bcthlem33 10175  grpoidinvlem3 10199  grpoidinv 10201  grpoideu 10202  grporcan 10216  grpoinveu 10217  isgrp2i 10229  grpasscan1 10230  gxneg 10258  gxsuc 10264  gxnn0add 10266  gxadd 10267  gxmul 10270  isga 10319  ring2 10343  vacnlem3 10538  vacnlem6 10541  nmblolbii 10668  blocnilem 10673  phpar2 10692  phpar 10693  siii 10723  ubthlem5 10745  ubthlem10 10750  minveclem25 10784  minveclem26 10785  minveclem27 10786  minvecex 10793  minvecexOLD 10794  minveceu 10799  htthlem12 10849  pilem1 10891  pilem2 10892  sineq0 10936  sineq0OLD 10937  efifolem4 10950  shftefif1olem 10966  grothpw 11005  2bornot2b 11014  ghomid 11029  fiuni 11054  txcn 11062  txcnopab 11063  stoig2 11090  subtopmetlem 11093  subtopmet 11094  fbssint 11117  fbunfip 11120  fgfil 11128  extbas1 11129  filrn 11131  flimfneii 11158  cncomp 11169  dirref 11193  dirtr 11194  exidu1 11211  rnplrnml0 11240  on1el3 11250  uznzr 11254  hlimcauii 11573  ocorth 11631  projlem25 11677  projlem26 11678  projlem31 11683  pjthlem11 11696  omlsii 11712  pjpj0i 11722  osumlem7 12051  spansncvi 12064  5oalem6 12071  unop 12308  hmop 12315  nmopun 12408  lnopconi 12432  lnfnconi 12459  nlelchi 12463  cnlnssadj 12482  rnbra 12509  cnvbraval 12512  leopmul 12536  nmopleid 12541  opsqrlem1 12542  hmopidmchlem 12553  hmopidmchi 12554  hstel2 12622  stcltrlem2 12680  csmdsymi 12737  atsseq 12750  atcveq0 12751  hatomistici 12765  cvati 12769  atexch 12784  atomli 12785  atcvati 12789  irredlem2 12794  irredlem4 12796  irredi 12797  atmd 12802  mdsymlem3 12808  mdsymlem5 12810  sumdmdlem 12821  cdj3lem2b 12840  addltmulALT 12849  bnj1050 13660  bnj1072 13673  bnj1210 13756  bnj578 14062  bnj605 14063  bnj594 14071  bnj944 14111  bnj1128 14199  bnj1125 14201  bnj1145 14202  bnj1154 14209  bnj1388 14285  bnj1417 14301  gch-aclem1 14353  prmdvdsexpbOLD 14355  cayleylem2 14379  sindivcvglem1 14386  sindivcvglem7 14392  sindivcvglem8 14393  elresOLD 14454  fundmpss 14467  dfon2lem3 14485  dfon2lem6 14488  dfon2lem8 14490  soxpOLD 14603  frxpOLD 14604  poseq 14607  wfrlem10 14619  sltres 14670  axdenselem5 14692  axdenselem7 14694  axfelem13 14711  axfelem18 14716  axfelem20 14718  axfelem22 14720  findreccl 14954  eloi 15112  fopab2g 15219  cbicplem 15247  supdef 15343  gaplc 15466  curgrpact 15470  grpdivone 15471  elsubops 15634  hmphre 15641  hmeogrp 15649  top2ind 15654  cmptdst 15717  grphm 15774  altretop 15788  cntrsetlem 15791  trnij 15807  lvsovso 15832  dualcat2lem 15923  homib 15939  idfisf 15983  idsubfun 16000  tarax3d2 16035  cptarc 16052  tarsuc2 16055  intartar 16065  carinttar2 16090  ecase13d 16174  fictb 16195  finsschain 16197  ordisoOLD 16198  ordtypelem6OLD 16204  ordtypelem7OLD 16205  onsdomOLD 16209  omsubelOLD 16216  omsublimOLD 16220  infenomsubOLD 16222  omsubinitOLD 16223  subcls 16248  subntr 16249  compsublem 16254  compsub 16255  cptclsscpt 16256  hscptsscld 16258  alexsublem4 16264  dfcon2 16266  connsub 16267  reconnlem1 16270  reconnlem4 16273  reconnlem5 16274  reconn 16275  ivthALT 16278  1stcclb 16295  2ndcctbss 16302  fnetr 16319  reftr 16321  topfneec 16325  fnessref 16327  locfincomp 16338  locfincf 16340  neibastop2 16347  topmeet 16350  fnemeet1 16352  fnemeet2 16353  fbasfip 16380  filfinnfr 16385  filssufil 16395  uffinfix 16401  ufinffr 16402  ufilen 16403  ufcondr 16405  limfilcf 16411  cnpfillim 16413  fmfnfm 16422  fmufil 16423  fcluscf 16436  fcluscnp 16442  fcluscomp 16445  ufcomp 16446  tailfb 16463  filnetlem3 16466  filnet 16469  unirep 16488  enf1f1o 16544  fimaxOLD 16570  fisupgOLD 16572  indexfiOLD 16579  fipreimaOLD 16580  inficl 16581  frinfm 16582  fisup2gOLD 16592  fimax2gOLD 16593  fimaxre 16598  fimaxre2 16599  divexp 16603  uzp1 16609  fzm1 16620  absz 16621  rddif 16622  absrdbnd 16623  absmod0 16626  sdc 16635  fdc 16636  fdc1 16637  incsequz2 16640  fsumlt 16645  fsumlt1 16655  blhalf 16670  mettrifi 16671  mettrifi2 16672  geomcau 16673  hmeocnv 16722  haustlmu 16730  cnresoprab 16739  sstotbnd 16760  totbndss 16761  totbndbnd 16768  ismtyhmeolem 16774  ismtybndlem 16776  heiborlem1 16779  heiborlem11 16789  heiborlem16 16794  heiborlem28 16806  heiborlem32 16810  heiborlem33 16811  heiborlem35 16813  heiborlem36 16814  heiborlem37 16815  heiborlem40 16818  rrncms 16843  ringneglmul 16928  ringnegrmul 16929  rngisocnv 16959  igenval 17033  isfldidl 17040  pridlc2 17044  pridlc3 17045  smogeOLD 17276  addrcom 17297  cmtbr4 17649  cvrcmp 17674  leat2 17684  meetat2 17686  atnleOLD 17713  atnle 17714  atlatmstc 17716  cvlcvr1 17736  cvlsupr2 17740  hlhgt2 17783  hl0lt1 17784  hl1at 17785  hl2at 17800  hlrelat3 17807  cvrval3 17808  cvrexchlem 17814  cvratlem 17816  cvrat 17817  atleOLD 17831  atle 17832  2atslt 17835  cvrat3 17838  atbtwnexOLD 17843  atbtwnex 17844  athgt 17852  3dim1 17863  3dim2 17864  3dim3 17865  2dim 17866  1cvratex 17869  1cvratlt 17870  ps-2 17874  ps-2b 17875  llnnleat 17945  llnn0 17948  llnle 17950  atcvrlln2 17951  atcvrlln 17952  llnexatOLD 17953  llncmp 17955  2llnmat 17957  llnmlpln 17970  lplnm2atOLD 17971  lplnle 17972  lplnnle2at 17973  lplnnlelln 17975  lplnn0 17979  lplnllnne 17988  llncvrlpln2 17989  llncvrlpln 17990  lplncmp 17994  lplnexlln 17996  2llnja 17998  2llnj 17999  lvolnle3at 18014  lvolnlelln 18016  lvolnlelpln 18017  lvoln0 18023  4atlem10 18038  4atlem11 18041  4atlem12 18044  lplncvrlvol2 18047  lplncvrlvol 18048  lvolcmp 18049  2lplnja 18051  2lplnj 18052  dalempnes 18083  dalemqnet 18084  dalem1 18091  dalemcea 18092  dalem3 18096  dalem5 18099  dalem-cly 18103  dalem20 18125  dalem25 18130  dalem27 18131  dalem28 18132  dalem44 18148  dalem62 18166  lneq2at 18210  lnatex 18211  lnjat 18212  lncvrat 18214  lncmp 18215  2lnat 18216  2llnma3r 18220  cdlema1 18223  cdlemblem 18225  cdlemb 18226  paddasslem10 18261  paddasslem15 18266  llnexchb2lem 18300  llnexchb2 18301  dalawlem2 18304  dalawlem3 18305  dalawlem6 18308  dalawlem7 18309  dalawlem11 18313  dalawlem12 18314  osumcllem4 18372  osumcllem7 18375  pexmidlem1 18383  pexmidlem4 18386  lhp0lt 18415  lhpne0 18416  lhp2at 18419  lhp2atex 18420  lhpj1 18428  lhprelat3 18435  ltrnu 18474  4atexlemunv 18536  4atexlemex2 18541  4atexlemcnd 18542  4atexlemex6 18544  trlnid 18548  ltrnnidn 18549  trlne 18553  trlval4 18556  cdlemd4OLD 18569  cdlemd9 18574  cdleme1 18596  cdleme3b 18599  cdleme9 18624  cdleme11d 18633  cdleme11g 18636  cdleme11h 18637  cdleme11j 18638  cdleme11l 18640  cdleme14 18644  cdleme16b 18650  cdleme18d 18666  cdlemednpq 18670  cdlemednu 18671  cdleme19a 18675  cdleme20d 18684  cdleme20f 18686  cdleme20j 18690  cdleme20k 18691  cdleme21at 18700  cdleme21ct 18701  cdleme21j 18708  cdleme22b 18713  cdleme22c 18714  cdleme22d 18715  cdleme22f 18718  cdleme22f2 18719  cdleme22g 18720  cdleme25a 18725  cdleme26ee 18732  cdleme27a 18739  cdleme28a 18742  cdleme29ex 18747  cdleme30a 18751  cdlemefr29ex 18776  cdleme32c 18819  cdleme32d 18820  cdleme32e 18821  cdleme32f 18822  cdleme35f 18830  cdleme35h2 18833  cdleme38n 18840  cdleme17d3 18877  cdlemeg46rgv 18911  cdlemeg46rgvOLD 18912  cdlemeg46gfre 18917  cdleme48gfv1 18921  cdleme50trn2 18936  cdleme51finvfv 18940  cdlemf1 18946  cdlemf2 18947  cdlemf 18948  cdlemg1cex 18963  cdlemgfvawOLD 18964  cdlemg2invOLD 18965  cdlemg2ce 18970  cdlemg5 18985  cdlemg7fvbw 18987  cdlemg6e 19002  cdlemg7a 19006  cdlemg8c 19010  cdlemg9 19015  cdlemg11a 19018  cdlemg11b 19023  cdlemg12 19026

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

Copyright terms: Public domain