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  1624  minimp-ax2c  1626  minimp-ax2  1627  minimp-pm2.43  1628  darii  2666  barbarilem  2669  festino  2675  baroco  2677  darapti  2685  sstri  3932  0disj  5079  disjx0  5081  opthhausdorff  5463  relres  5962  cnvdif  6099  difxp  6120  funopab4  6527  fun0  6555  omsinds  7829  frxp3  8092  reltpos  8172  tpos0  8197  oaabs2  8576  swoer  8666  xpider  8726  sbthcl  9028  elirrvOLD  9504  unctb  10115  fin1a2lem12  10322  axcc2lem  10347  axcclem  10368  brdom3  10439  brdom5  10440  brdom4  10441  pwcfsdom  10495  smobeth  10498  pwxpndom2  10577  pwdjundom  10579  gchac  10593  wunex3  10653  inar1  10687  gruina  10730  ltsopi  10800  recmulnq  10876  prcdnq  10905  ltrel  11196  lerel  11198  suprfinzcl  12632  cnexALT  12925  dfle2  13087  dflt2  13088  uzrdg0i  13910  ltwefz  13914  fzennn  13919  faclbnd4lem1  14244  hashsslei  14377  0csh0  14744  isercolllem1  15616  zsum  15669  sum0  15672  znnen  16168  qnnen  16169  rpnnen  16183  ruc  16199  nthruc  16208  nthruz  16209  phicl2  16727  relfull  17866  relfth  17867  gicer  19241  oppglsm  19606  efgrelexlemb  19714  isunit  20342  xrsnsgrp  21395  pjpm  21696  1stcfb  23419  2ndc1stc  23425  2ndcctbss  23429  2ndcdisj2  23431  2ndcsep  23433  hmpher  23758  met1stc  24495  re2ndc  24775  iccpnfhmeo  24921  xrhmeo  24922  xrcmp  24924  xrconn  24925  dyadmbl  25576  opnmblALT  25579  vitalilem2  25585  vitalilem3  25586  vitali  25589  mbfimaopnlem  25631  mbfsup  25640  dgrval  26205  dgrcl  26210  dgrub  26211  dgrlb  26213  aannenlem3  26309  dvrelog  26617  logcn  26627  logccv  26643  ppiub  27186  lgsquadlem1  27362  lgsquadlem2  27363  addsqrexnreu  27424  addsqnreup  27425  2sqreunnlem2  27437  dirith2  27510  madefi  27924  bdayfinbndlem1  28478  usgrexmpldifpr  29346  usgrexmplef  29347  disjxwwlksn  29992  disjxwwlkn  30001  nvrel  30693  phrel  30906  bnrel  30958  hlrel  30981  pjnormi  31812  lnopunilem1  32101  lnophmlem1  32107  xrge0infssd  32854  infxrge0lb  32857  infxrge0glb  32858  infxrge0gelb  32859  ssnnssfz  32880  xrge0iifiso  34100  omsf  34461  oms0  34462  omssubaddlem  34464  omssubadd  34465  oddpwdc  34519  rpsqrtcn  34758  bnj1023  34944  bnj1109  34950  erdszelem4  35397  erdszelem8  35401  gonan0  35595  2thALT  35887  supfz  35932  inffz  35933  trer  36519  fneer  36556  naim1i  36594  naim2i  36595  nmotru  36611  onpsstopbas  36633  bj-mp2c  36813  bj-mp2d  36814  bj-bijust00  36855  bj-almp  36889  bj-axseprep  37394  iccioo01  37654  pibt2  37744  wl-equsal1i  37880  wl-sbcom2d  37897  poimirlem25  37977  poimirlem26  37978  mblfinlem1  37989  incsequz2  38081  cncfres  38097  heiborlem3  38145  diclspsn  41651  dih1dimatlem  41786  rencldnfilem  43263  pellexlem4  43275  pellexlem5  43276  ttac  43479  idomsubgmo  43636  areaquad  43659  frege102  44407  lhe4.4ex1a  44771  eel0000  45161  eel00001  45162  eel00000  45163  e000  45208  e00  45209  wffr  45403  modelaxreplem1  45420  nregmodellem  45458  fzisoeu  45748  resincncf  46318  nthrucw  47329  aiota0def  47541  fvmptrabdm  47738  fmtnoinf  47996  gricrel  48392  grlicrel  48479  usgrexmpl1lem  48494  usgrexmpl2lem  48499  usgrexmpl2nb0  48504  usgrexmpl2nb1  48505  usgrexmpl2nb2  48506  usgrexmpl2nb3  48507  usgrexmpl2nb4  48508  usgrexmpl2nb5  48509  gpgprismgr4cycllem2  48569  gpg5ngric  48601  ssnn0ssfz  48822  zlmodzxzldeplem  48971  tposideq  49360