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  470  minimp-syllsimp  1616  minimp-ax2c  1618  minimp-ax2  1619  minimp-pm2.43  1620  darii  2652  barbarilem  2655  festino  2661  baroco  2663  darapti  2671  sstri  3983  0disj  5130  disjx0  5132  opthhausdorff  5507  relres  6000  cnvdif  6133  difxp  6153  funopab4  6575  fun0  6603  omsinds  7869  omsindsOLD  7870  frxp3  8131  reltpos  8211  tpos0  8236  oaabs2  8644  swoer  8729  xpider  8778  sbthcl  9091  phpOLD  9218  elirrv  9587  unctb  10196  fin1a2lem12  10402  axcc2lem  10427  axcclem  10448  brdom3  10519  brdom5  10520  brdom4  10521  pwcfsdom  10574  smobeth  10577  pwxpndom2  10656  pwdjundom  10658  gchac  10672  wunex3  10732  inar1  10766  gruina  10809  ltsopi  10879  recmulnq  10955  prcdnq  10984  ltrel  11273  lerel  11275  suprfinzcl  12673  cnexALT  12967  dfle2  13123  dflt2  13124  uzrdg0i  13921  ltwefz  13925  fzennn  13930  faclbnd4lem1  14250  hashsslei  14383  0csh0  14740  isercolllem1  15608  zsum  15661  sum0  15664  znnen  16152  qnnen  16153  rpnnen  16167  ruc  16183  nthruc  16192  nthruz  16193  phicl2  16700  relfull  17860  relfth  17861  gicer  19192  oppglsm  19552  efgrelexlemb  19660  isunit  20265  xrsnsgrp  21265  pjpm  21571  1stcfb  23271  2ndc1stc  23277  2ndcctbss  23281  2ndcdisj2  23283  2ndcsep  23285  hmpher  23610  met1stc  24352  re2ndc  24639  iccpnfhmeo  24792  xrhmeo  24793  xrcmp  24795  xrconn  24796  dyadmbl  25451  opnmblALT  25454  vitalilem2  25460  vitalilem3  25461  vitali  25464  mbfimaopnlem  25506  mbfsup  25515  dgrval  26082  dgrcl  26087  dgrub  26088  dgrlb  26090  aannenlem3  26184  dvrelog  26487  logcn  26497  logccv  26513  ppiub  27053  lgsquadlem1  27229  lgsquadlem2  27230  addsqrexnreu  27291  addsqnreup  27292  2sqreunnlem2  27304  dirith2  27377  usgrexmpldifpr  28984  usgrexmplef  28985  disjxwwlksn  29627  disjxwwlkn  29636  nvrel  30324  phrel  30537  bnrel  30589  hlrel  30612  pjnormi  31443  lnopunilem1  31732  lnophmlem1  31738  xrge0infssd  32443  infxrge0lb  32446  infxrge0glb  32447  infxrge0gelb  32448  ssnnssfz  32467  xrge0iifiso  33404  omsf  33784  oms0  33785  omssubaddlem  33787  omssubadd  33788  oddpwdc  33842  rpsqrtcn  34094  bnj1023  34280  bnj1109  34286  erdszelem4  34674  erdszelem8  34678  gonan0  34872  supfz  35193  inffz  35194  trer  35691  fneer  35728  naim1i  35766  naim2i  35767  nmotru  35783  onpsstopbas  35805  bj-mp2c  35906  bj-mp2d  35907  bj-bijust00  35944  bj-cbvalim  36012  bj-cbvexim  36013  bj-cbvalimi  36014  bj-cbveximi  36015  iccioo01  36698  pibt2  36788  wl-equsal1i  36902  wl-sbcom2d  36916  poimirlem25  37003  poimirlem26  37004  mblfinlem1  37015  incsequz2  37107  cncfres  37123  heiborlem3  37171  diclspsn  40555  dih1dimatlem  40690  rencldnfilem  42047  pellexlem4  42059  pellexlem5  42060  ttac  42264  idomsubgmo  42429  areaquad  42454  frege102  43205  lhe4.4ex1a  43577  eel0000  43970  eel00001  43971  eel00000  43972  e000  44017  e00  44018  fzisoeu  44495  resincncf  45076  aiota0def  46289  fvmptrabdm  46486  fmtnoinf  46689  ssnn0ssfz  47214  zlmodzxzldeplem  47367