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  353  pm3.2i  475  minimp-syllsimp  1650  minimp-ax2c  1652  minimp-ax2  1653  minimp-pm2.43  1654  darii  2690  barbarilem  2693  festino  2699  baroco  2701  darapti  2709  sstri  3945  0disj  5101  disjx0  5103  opthhausdorff  5500  relres  6004  cnvdif  6140  difxp  6161  funopab4  6573  fun0  6601  omsinds  7882  frxp3  8146  reltpos  8226  tpos0  8251  oaabs2  8634  swoer  8725  xpider  8785  sbthcl  9086  elirrvOLDOLD  9560  unctb  10186  fin1a2lem12  10394  axcc2lem  10419  axcclem  10440  brdom3  10511  brdom5  10512  brdom4  10513  pwcfsdom  10567  smobeth  10570  pwxpndom2  10649  pwdjundom  10651  gchac  10665  wunex3  10725  inar1  10759  gruina  10802  ltsopi  10872  recmulnq  10948  prcdnq  10977  ltrel  11270  lerel  11272  suprfinzcl  12709  cnexALT  13009  dfle2  13171  dflt2  13172  uzrdg0i  13995  ltwefz  13999  fzennn  14004  faclbnd4lem1  14329  hashsslei  14463  0csh0  14830  isercolllem1  15716  zsum  15769  sum0  15772  znnen  16267  qnnen  16268  rpnnen  16282  ruc  16298  nthruc  16307  nthruz  16308  phicl2  16826  relfull  17966  relfth  17967  gicer  19346  oppglsm  19711  efgrelexlemb  19819  isunit  20454  xrsnsgrp  21537  pjpm  21837  1stcfb  23581  2ndc1stc  23587  2ndcctbss  23591  2ndcdisj2  23593  2ndcsep  23595  hmpher  23920  met1stc  24657  re2ndc  24937  iccpnfhmeo  25083  xrhmeo  25084  xrcmp  25086  xrconn  25087  dyadmbl  25738  opnmblALT  25741  vitalilem2  25747  vitalilem3  25748  vitali  25751  mbfimaopnlem  25793  mbfsup  25802  dgrval  26364  dgrcl  26369  dgrub  26370  dgrlb  26372  aannenlem3  26470  dvrelog  26778  logcn  26788  logccv  26804  ppiub  27344  lgsquadlem1  27520  lgsquadlem2  27521  addsqrexnreu  27582  addsqnreup  27583  2sqreunnlem2  27595  dirith2  27668  madefi  28082  bdayfinbndlem1  28636  usgrexmpldifpr  29574  usgrexmplef  29575  disjxwwlksn  30219  disjxwwlkn  30228  nvrel  30920  phrel  31133  bnrel  31185  hlrel  31208  pjnormi  32039  lnopunilem1  32328  lnophmlem1  32334  xrge0infssd  33072  infxrge0lb  33075  infxrge0glb  33076  infxrge0gelb  33077  ssnnssfz  33098  xrge0iifiso  34291  omsf  34652  oms0  34653  omssubaddlem  34655  omssubadd  34656  oddpwdc  34710  rpsqrtcn  34946  bnj1023  35135  bnj1109  35141  erdszelem4  35652  erdszelem8  35656  gonan0  35850  2thALT  36142  supfz  36187  inffz  36188  trer  36793  fneer  36830  naim1i  36868  naim2i  36869  nmotru  36885  onpsstopbas  36907  bj-mp2c  37095  bj-mp2d  37096  bj-bijust00  37136  bj-almp  37170  bj-axseprep  37677  iccioo01  37939  pibt2  38029  wl-equsal1i  38165  wl-sbcom2d  38182  poimirlem25  38262  poimirlem26  38263  mblfinlem1  38274  incsequz2  38366  cncfres  38382  heiborlem3  38430  diclspsn  41936  dih1dimatlem  42071  rencldnfilem  43517  pellexlem4  43529  pellexlem5  43530  ttac  43733  idomsubgmo  43890  areaquad  43913  frege102  44661  lhe4.4ex1a  45009  eel0000  45398  eel00001  45399  eel00000  45400  e000  45445  e00  45446  wffr  45640  modelaxreplem1  45657  nregmodellem  45695  fzisoeu  45989  resincncf  46559  nthrucw  47572  aiota0def  47800  fvmptrabdm  47997  fmtnoinf  48255  gricrel  48651  grlicrel  48738  usgrexmpl1lem  48753  usgrexmpl2lem  48758  usgrexmpl2nb0  48763  usgrexmpl2nb1  48764  usgrexmpl2nb2  48765  usgrexmpl2nb3  48766  usgrexmpl2nb4  48767  usgrexmpl2nb5  48768  gpgprismgr4cycllem2  48828  gpg5ngric  48860  ssnn0ssfz  49096  zlmodzxzldeplem  49245  tposideq  49633