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  208  imbi12i  350  pm3.2i  471  minimp-syllsimp  1624  minimp-ax2c  1626  minimp-ax2  1627  minimp-pm2.43  1628  darii  2659  barbarilem  2662  festino  2668  baroco  2670  darapti  2678  sstri  3956  0disj  5102  disjx0  5104  opthhausdorff  5479  relres  5971  cnvdif  6101  difxp  6121  funopab4  6543  fun0  6571  omsinds  7828  omsindsOLD  7829  frxp3  8088  reltpos  8167  tpos0  8192  oaabs2  8600  swoer  8685  xpider  8734  sbthcl  9046  phpOLD  9173  elirrv  9541  unctb  10150  fin1a2lem12  10356  axcc2lem  10381  axcclem  10402  brdom3  10473  brdom5  10474  brdom4  10475  pwcfsdom  10528  smobeth  10531  pwxpndom2  10610  pwdjundom  10612  gchac  10626  wunex3  10686  inar1  10720  gruina  10763  ltsopi  10833  recmulnq  10909  prcdnq  10938  ltrel  11226  lerel  11228  suprfinzcl  12626  cnexALT  12920  dfle2  13076  dflt2  13077  uzrdg0i  13874  ltwefz  13878  fzennn  13883  faclbnd4lem1  14203  hashsslei  14336  0csh0  14693  isercolllem1  15561  zsum  15614  sum0  15617  znnen  16105  qnnen  16106  rpnnen  16120  ruc  16136  nthruc  16145  nthruz  16146  phicl2  16651  relfull  17809  relfth  17810  gicer  19080  oppglsm  19438  efgrelexlemb  19546  isunit  20100  xrsnsgrp  20870  pjpm  21151  1stcfb  22833  2ndc1stc  22839  2ndcctbss  22843  2ndcdisj2  22845  2ndcsep  22847  hmpher  23172  met1stc  23914  re2ndc  24201  iccpnfhmeo  24345  xrhmeo  24346  xrcmp  24348  xrconn  24349  dyadmbl  25001  opnmblALT  25004  vitalilem2  25010  vitalilem3  25011  vitali  25014  mbfimaopnlem  25056  mbfsup  25065  dgrval  25626  dgrcl  25631  dgrub  25632  dgrlb  25634  aannenlem3  25727  dvrelog  26029  logcn  26039  logccv  26055  ppiub  26589  lgsquadlem1  26765  lgsquadlem2  26766  addsqrexnreu  26827  addsqnreup  26828  2sqreunnlem2  26840  dirith2  26913  usgrexmpldifpr  28269  usgrexmplef  28270  disjxwwlksn  28912  disjxwwlkn  28921  nvrel  29607  phrel  29820  bnrel  29872  hlrel  29895  pjnormi  30726  lnopunilem1  31015  lnophmlem1  31021  xrge0infssd  31734  infxrge0lb  31737  infxrge0glb  31738  infxrge0gelb  31739  ssnnssfz  31758  xrge0iifiso  32605  omsf  32985  oms0  32986  omssubaddlem  32988  omssubadd  32989  oddpwdc  33043  rpsqrtcn  33295  bnj1023  33481  bnj1109  33487  erdszelem4  33875  erdszelem8  33879  gonan0  34073  supfz  34387  inffz  34388  trer  34864  fneer  34901  naim1i  34939  naim2i  34940  nmotru  34956  onpsstopbas  34978  bj-mp2c  35079  bj-mp2d  35080  bj-bijust00  35117  bj-cbvalim  35185  bj-cbvexim  35186  bj-cbvalimi  35187  bj-cbveximi  35188  iccioo01  35871  pibt2  35961  wl-equsal1i  36075  wl-sbcom2d  36089  poimirlem25  36176  poimirlem26  36177  mblfinlem1  36188  incsequz2  36281  cncfres  36297  heiborlem3  36345  diclspsn  39730  dih1dimatlem  39865  rencldnfilem  41201  pellexlem4  41213  pellexlem5  41214  ttac  41418  idomsubgmo  41583  areaquad  41608  frege102  42359  lhe4.4ex1a  42731  eel0000  43124  eel00001  43125  eel00000  43126  e000  43171  e00  43172  fzisoeu  43655  resincncf  44236  aiota0def  45448  fvmptrabdm  45645  fmtnoinf  45848  ssnn0ssfz  46545  zlmodzxzldeplem  46699