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  201  imbi12i  342  pm3.2i  464  minimp-syllsimp  1737  minimp-ax2c  1739  minimp-ax2  1740  minimp-pm2.43  1741  sbcom2OLD  2578  darii  2747  barbarilem  2750  festino  2758  baroco  2760  darapti  2772  sstri  3835  0disj  4865  disjx0  4867  opthhausdorff  5202  relres  5661  cnvdif  5779  difxp  5798  funopab4  6159  fun0  6186  fvsnOLD  6699  omsinds  7344  reltpos  7621  tpostpos  7636  tpos0  7646  oaabs2  7991  swoer  8038  xpider  8082  sbthcl  8350  php  8412  elirrv  8769  inf0  8794  unctb  9341  fin1a2lem12  9547  axcc2lem  9572  axcclem  9593  brdom3  9664  brdom5  9665  brdom4  9666  pwcfsdom  9719  smobeth  9722  pwxpndom2  9801  pwcdandom  9803  gchac  9817  wunex3  9877  inar1  9911  gruina  9954  ltsopi  10024  recmulnq  10100  prcdnq  10129  ltrel  10418  lerel  10420  suprfinzcl  11819  cnexALT  12107  dfle2  12265  dflt2  12266  uzrdg0i  13052  ltwefz  13056  fzennn  13061  faclbnd4lem1  13372  hashsslei  13501  0csh0  13912  0csh0OLD  13913  isercolllem1  14771  zsum  14825  sum0  14828  znnen  15314  qnnen  15315  rpnnen  15329  ruc  15345  nthruc  15354  nthruz  15355  phicl2  15843  xpsc0  16572  xpsc1  16573  relfull  16919  relfth  16920  gicer  18068  oppglsm  18407  efgrelexlemb  18515  isunit  19010  opsrtoslem2  19844  xrsnsgrp  20141  pjpm  20414  1stcfb  21618  2ndc1stc  21624  2ndcctbss  21628  2ndcdisj2  21630  2ndcsep  21632  hmpher  21957  met1stc  22695  re2ndc  22973  iccpnfhmeo  23113  xrhmeo  23114  xrcmp  23116  xrconn  23117  dyadmbl  23765  opnmblALT  23768  vitalilem2  23774  vitalilem3  23775  vitali  23778  mbfimaopnlem  23820  mbfsup  23829  dgrval  24382  dgrcl  24387  dgrub  24388  dgrlb  24390  aannenlem3  24483  dvrelog  24781  logcn  24791  logccv  24807  logblog  24931  ppiub  25341  lgsquadlem1  25517  lgsquadlem2  25518  dirith2  25629  usgrexmpldifpr  26554  usgrexmplef  26555  disjxwwlksn  27224  disjxwwlksnOLD  27225  disjxwwlkn  27239  disjxwwlknOLD  27240  nvrel  28011  phrel  28224  bnrel  28277  hlrel  28300  pjnormi  29134  lnopunilem1  29423  lnophmlem1  29429  xrge0infssd  30072  infxrge0lb  30075  infxrge0glb  30076  infxrge0gelb  30077  ssnnssfz  30095  xrge0iifiso  30525  omsf  30902  oms0  30903  omssubaddlem  30905  omssubadd  30906  oddpwdc  30960  rpsqrtcn  31219  bnj1023  31396  bnj1109  31402  erdszelem4  31721  erdszelem8  31725  supfz  32155  inffz  32156  elrn3  32193  trer  32848  fneer  32885  naim1i  32923  naim2i  32924  nmotru  32940  onpsstopbas  32961  bj-mp2c  33062  bj-mp2d  33063  bj-currypeirce  33073  bj-bijust00  33089  bj-cbvalim  33148  bj-cbvalimi  33149  wl-equsal1i  33872  wl-sbcom2d  33887  poimirlem25  33977  poimirlem26  33978  mblfinlem1  33989  incsequz2  34086  cncfres  34105  heiborlem3  34153  diclspsn  37268  dih1dimatlem  37403  rencldnfilem  38227  pellexlem4  38239  pellexlem5  38240  ttac  38445  idomsubgmo  38618  areaquad  38643  frege102  39098  lhe4.4ex1a  39367  eel0001  39772  eel0000  39773  eel00001  39774  eel00000  39775  e000  39820  e00  39821  fzisoeu  40311  resincncf  40882  aiota0def  41990  fvmptrabdm  42195  fmtnoinf  42277  ssnn0ssfz  42973  zlmodzxzldeplem  43133