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  5472  relres  5971  cnvdif  6108  difxp  6129  funopab4  6536  fun0  6564  omsinds  7838  frxp3  8101  reltpos  8181  tpos0  8206  oaabs2  8585  swoer  8675  xpider  8735  sbthcl  9037  elirrvOLD  9513  unctb  10126  fin1a2lem12  10333  axcc2lem  10358  axcclem  10379  brdom3  10450  brdom5  10451  brdom4  10452  pwcfsdom  10506  smobeth  10509  pwxpndom2  10588  pwdjundom  10590  gchac  10604  wunex3  10664  inar1  10698  gruina  10741  ltsopi  10811  recmulnq  10887  prcdnq  10916  ltrel  11207  lerel  11209  suprfinzcl  12643  cnexALT  12936  dfle2  13098  dflt2  13099  uzrdg0i  13921  ltwefz  13925  fzennn  13930  faclbnd4lem1  14255  hashsslei  14388  0csh0  14755  isercolllem1  15627  zsum  15680  sum0  15683  znnen  16179  qnnen  16180  rpnnen  16194  ruc  16210  nthruc  16219  nthruz  16220  phicl2  16738  relfull  17877  relfth  17878  gicer  19252  oppglsm  19617  efgrelexlemb  19725  isunit  20353  xrsnsgrp  21388  pjpm  21688  1stcfb  23410  2ndc1stc  23416  2ndcctbss  23420  2ndcdisj2  23422  2ndcsep  23424  hmpher  23749  met1stc  24486  re2ndc  24766  iccpnfhmeo  24912  xrhmeo  24913  xrcmp  24915  xrconn  24916  dyadmbl  25567  opnmblALT  25570  vitalilem2  25576  vitalilem3  25577  vitali  25580  mbfimaopnlem  25622  mbfsup  25631  dgrval  26193  dgrcl  26198  dgrub  26199  dgrlb  26201  aannenlem3  26296  dvrelog  26601  logcn  26611  logccv  26627  ppiub  27167  lgsquadlem1  27343  lgsquadlem2  27344  addsqrexnreu  27405  addsqnreup  27406  2sqreunnlem2  27418  dirith2  27491  madefi  27905  bdayfinbndlem1  28459  usgrexmpldifpr  29327  usgrexmplef  29328  disjxwwlksn  29972  disjxwwlkn  29981  nvrel  30673  phrel  30886  bnrel  30938  hlrel  30961  pjnormi  31792  lnopunilem1  32081  lnophmlem1  32087  xrge0infssd  32834  infxrge0lb  32837  infxrge0glb  32838  infxrge0gelb  32839  ssnnssfz  32860  xrge0iifiso  34079  omsf  34440  oms0  34441  omssubaddlem  34443  omssubadd  34444  oddpwdc  34498  rpsqrtcn  34737  bnj1023  34923  bnj1109  34929  erdszelem4  35376  erdszelem8  35380  gonan0  35574  2thALT  35866  supfz  35911  inffz  35912  trer  36498  fneer  36535  naim1i  36573  naim2i  36574  nmotru  36590  onpsstopbas  36612  bj-mp2c  36800  bj-mp2d  36801  bj-bijust00  36842  bj-almp  36876  bj-axseprep  37381  iccioo01  37643  pibt2  37733  wl-equsal1i  37869  wl-sbcom2d  37886  poimirlem25  37966  poimirlem26  37967  mblfinlem1  37978  incsequz2  38070  cncfres  38086  heiborlem3  38134  diclspsn  41640  dih1dimatlem  41775  rencldnfilem  43248  pellexlem4  43260  pellexlem5  43261  ttac  43464  idomsubgmo  43621  areaquad  43644  frege102  44392  lhe4.4ex1a  44756  eel0000  45146  eel00001  45147  eel00000  45148  e000  45193  e00  45194  wffr  45388  modelaxreplem1  45405  nregmodellem  45443  fzisoeu  45733  resincncf  46303  nthrucw  47314  aiota0def  47538  fvmptrabdm  47735  fmtnoinf  47993  gricrel  48389  grlicrel  48476  usgrexmpl1lem  48491  usgrexmpl2lem  48496  usgrexmpl2nb0  48501  usgrexmpl2nb1  48502  usgrexmpl2nb2  48503  usgrexmpl2nb3  48504  usgrexmpl2nb4  48505  usgrexmpl2nb5  48506  gpgprismgr4cycllem2  48566  gpg5ngric  48598  ssnn0ssfz  48819  zlmodzxzldeplem  48968  tposideq  49357