Theorem mp2 9

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)

Hypotheses

Ref	Expression
mp2.1	⊢ 𝜑
mp2.2	⊢ 𝜓
mp2.3	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mp2	⊢ 𝜒

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.2	. 2 ⊢ 𝜓
2		mp2.1	. . 3 ⊢ 𝜑
3		mp2.3	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	ax-mp 5	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  impbii  209  imbi12i  350  pm3.2i  470  minimp-syllsimp  1622  minimp-ax2c  1624  minimp-ax2  1625  minimp-pm2.43  1626  darii  2659  barbarilem  2662  festino  2668  baroco  2670  darapti  2678  sstri  3959  0disj  5103  disjx0  5105  opthhausdorff  5480  relres  5979  cnvdif  6119  difxp  6140  funopab4  6556  fun0  6584  omsinds  7866  frxp3  8133  reltpos  8213  tpos0  8238  oaabs2  8616  swoer  8705  xpider  8764  sbthcl  9069  elirrv  9556  unctb  10164  fin1a2lem12  10371  axcc2lem  10396  axcclem  10417  brdom3  10488  brdom5  10489  brdom4  10490  pwcfsdom  10543  smobeth  10546  pwxpndom2  10625  pwdjundom  10627  gchac  10641  wunex3  10701  inar1  10735  gruina  10778  ltsopi  10848  recmulnq  10924  prcdnq  10953  ltrel  11243  lerel  11245  suprfinzcl  12655  cnexALT  12952  dfle2  13114  dflt2  13115  uzrdg0i  13931  ltwefz  13935  fzennn  13940  faclbnd4lem1  14265  hashsslei  14398  0csh0  14765  isercolllem1  15638  zsum  15691  sum0  15694  znnen  16187  qnnen  16188  rpnnen  16202  ruc  16218  nthruc  16227  nthruz  16228  phicl2  16745  relfull  17879  relfth  17880  gicer  19216  oppglsm  19579  efgrelexlemb  19687  isunit  20289  xrsnsgrp  21326  pjpm  21624  1stcfb  23339  2ndc1stc  23345  2ndcctbss  23349  2ndcdisj2  23351  2ndcsep  23353  hmpher  23678  met1stc  24416  re2ndc  24696  iccpnfhmeo  24850  xrhmeo  24851  xrcmp  24853  xrconn  24854  dyadmbl  25508  opnmblALT  25511  vitalilem2  25517  vitalilem3  25518  vitali  25521  mbfimaopnlem  25563  mbfsup  25572  dgrval  26140  dgrcl  26145  dgrub  26146  dgrlb  26148  aannenlem3  26245  dvrelog  26553  logcn  26563  logccv  26579  ppiub  27122  lgsquadlem1  27298  lgsquadlem2  27299  addsqrexnreu  27360  addsqnreup  27361  2sqreunnlem2  27373  dirith2  27446  madefi  27831  usgrexmpldifpr  29192  usgrexmplef  29193  disjxwwlksn  29841  disjxwwlkn  29850  nvrel  30538  phrel  30751  bnrel  30803  hlrel  30826  pjnormi  31657  lnopunilem1  31946  lnophmlem1  31952  xrge0infssd  32691  infxrge0lb  32694  infxrge0glb  32695  infxrge0gelb  32696  ssnnssfz  32717  xrge0iifiso  33932  omsf  34294  oms0  34295  omssubaddlem  34297  omssubadd  34298  oddpwdc  34352  rpsqrtcn  34591  bnj1023  34777  bnj1109  34783  erdszelem4  35188  erdszelem8  35192  gonan0  35386  2thALT  35678  supfz  35723  inffz  35724  trer  36311  fneer  36348  naim1i  36386  naim2i  36387  nmotru  36403  onpsstopbas  36425  bj-mp2c  36535  bj-mp2d  36536  bj-bijust00  36572  bj-cbvalim  36640  bj-cbvexim  36641  bj-cbvalimi  36642  bj-cbveximi  36643  iccioo01  37322  pibt2  37412  wl-equsal1i  37539  wl-sbcom2d  37556  poimirlem25  37646  poimirlem26  37647  mblfinlem1  37658  incsequz2  37750  cncfres  37766  heiborlem3  37814  diclspsn  41195  dih1dimatlem  41330  rencldnfilem  42815  pellexlem4  42827  pellexlem5  42828  ttac  43032  idomsubgmo  43189  areaquad  43212  frege102  43961  lhe4.4ex1a  44325  eel0000  44716  eel00001  44717  eel00000  44718  e000  44763  e00  44764  wffr  44958  modelaxreplem1  44975  nregmodellem  45013  fzisoeu  45305  resincncf  45880  aiota0def  47101  fvmptrabdm  47298  fmtnoinf  47541  gricrel  47923  grlicrel  48002  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  gpgprismgr4cycllem2  48090  gpg5ngric  48122  ssnn0ssfz  48341  zlmodzxzldeplem  48491  tposideq  48880