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  212  imbi12i  354  pm3.2i  474  minimp-syllsimp  1629  minimp-ax2c  1631  minimp-ax2  1632  minimp-pm2.43  1633  darii  2667  barbarilem  2670  festino  2676  baroco  2678  darapti  2686  sstri  3886  0disj  5022  disjx0  5024  opthhausdorff  5374  relres  5854  cnvdif  5976  difxp  5996  funopab4  6376  fun0  6404  omsinds  7619  reltpos  7926  tpos0  7951  oaabs2  8303  swoer  8350  xpider  8399  sbthcl  8689  php  8751  elirrv  9133  unctb  9705  fin1a2lem12  9911  axcc2lem  9936  axcclem  9957  brdom3  10028  brdom5  10029  brdom4  10030  pwcfsdom  10083  smobeth  10086  pwxpndom2  10165  pwdjundom  10167  gchac  10181  wunex3  10241  inar1  10275  gruina  10318  ltsopi  10388  recmulnq  10464  prcdnq  10493  ltrel  10781  lerel  10783  suprfinzcl  12178  cnexALT  12468  dfle2  12623  dflt2  12624  uzrdg0i  13418  ltwefz  13422  fzennn  13427  faclbnd4lem1  13745  hashsslei  13879  0csh0  14244  isercolllem1  15114  zsum  15168  sum0  15171  znnen  15657  qnnen  15658  rpnnen  15672  ruc  15688  nthruc  15697  nthruz  15698  phicl2  16205  relfull  17283  relfth  17284  gicer  18534  oppglsm  18885  efgrelexlemb  18994  isunit  19529  xrsnsgrp  20253  pjpm  20524  1stcfb  22196  2ndc1stc  22202  2ndcctbss  22206  2ndcdisj2  22208  2ndcsep  22210  hmpher  22535  met1stc  23274  re2ndc  23553  iccpnfhmeo  23697  xrhmeo  23698  xrcmp  23700  xrconn  23701  dyadmbl  24352  opnmblALT  24355  vitalilem2  24361  vitalilem3  24362  vitali  24365  mbfimaopnlem  24407  mbfsup  24416  dgrval  24977  dgrcl  24982  dgrub  24983  dgrlb  24985  aannenlem3  25078  dvrelog  25380  logcn  25390  logccv  25406  ppiub  25940  lgsquadlem1  26116  lgsquadlem2  26117  addsqrexnreu  26178  addsqnreup  26179  2sqreunnlem2  26191  dirith2  26264  usgrexmpldifpr  27200  usgrexmplef  27201  disjxwwlksn  27842  disjxwwlkn  27851  nvrel  28537  phrel  28750  bnrel  28802  hlrel  28825  pjnormi  29656  lnopunilem1  29945  lnophmlem1  29951  xrge0infssd  30659  infxrge0lb  30662  infxrge0glb  30663  infxrge0gelb  30664  ssnnssfz  30683  xrge0iifiso  31457  omsf  31833  oms0  31834  omssubaddlem  31836  omssubadd  31837  oddpwdc  31891  rpsqrtcn  32143  bnj1023  32331  bnj1109  32337  erdszelem4  32727  erdszelem8  32731  gonan0  32925  supfz  33265  inffz  33266  trer  34143  fneer  34180  naim1i  34218  naim2i  34219  nmotru  34235  onpsstopbas  34257  bj-mp2c  34358  bj-mp2d  34359  bj-bijust00  34396  bj-cbvalim  34464  bj-cbvexim  34465  bj-cbvalimi  34466  bj-cbveximi  34467  iccioo01  35118  pibt2  35211  wl-equsal1i  35325  wl-sbcom2d  35339  poimirlem25  35425  poimirlem26  35426  mblfinlem1  35437  incsequz2  35530  cncfres  35546  heiborlem3  35594  diclspsn  38831  dih1dimatlem  38966  rencldnfilem  40214  pellexlem4  40226  pellexlem5  40227  ttac  40430  idomsubgmo  40595  areaquad  40619  frege102  41119  lhe4.4ex1a  41485  eel0000  41878  eel00001  41879  eel00000  41880  e000  41925  e00  41926  fzisoeu  42377  resincncf  42958  aiota0def  44120  fvmptrabdm  44318  fmtnoinf  44522  ssnn0ssfz  45219  zlmodzxzldeplem  45373