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  1624  minimp-ax2c  1626  minimp-ax2  1627  minimp-pm2.43  1628  darii  2727  barbarilem  2730  festino  2736  baroco  2738  darapti  2746  sstri  3924  0disj  5022  disjx0  5024  opthhausdorff  5372  relres  5847  cnvdif  5969  difxp  5988  funopab4  6361  fun0  6389  omsinds  7580  reltpos  7880  tpos0  7905  oaabs2  8255  swoer  8302  xpider  8351  sbthcl  8623  php  8685  elirrv  9044  unctb  9616  fin1a2lem12  9822  axcc2lem  9847  axcclem  9868  brdom3  9939  brdom5  9940  brdom4  9941  pwcfsdom  9994  smobeth  9997  pwxpndom2  10076  pwdjundom  10078  gchac  10092  wunex3  10152  inar1  10186  gruina  10229  ltsopi  10299  recmulnq  10375  prcdnq  10404  ltrel  10692  lerel  10694  suprfinzcl  12085  cnexALT  12373  dfle2  12528  dflt2  12529  uzrdg0i  13322  ltwefz  13326  fzennn  13331  faclbnd4lem1  13649  hashsslei  13783  0csh0  14146  isercolllem1  15013  zsum  15067  sum0  15070  znnen  15557  qnnen  15558  rpnnen  15572  ruc  15588  nthruc  15597  nthruz  15598  phicl2  16095  relfull  17170  relfth  17171  gicer  18408  oppglsm  18759  efgrelexlemb  18868  isunit  19403  xrsnsgrp  20127  pjpm  20397  1stcfb  22050  2ndc1stc  22056  2ndcctbss  22060  2ndcdisj2  22062  2ndcsep  22064  hmpher  22389  met1stc  23128  re2ndc  23406  iccpnfhmeo  23550  xrhmeo  23551  xrcmp  23553  xrconn  23554  dyadmbl  24204  opnmblALT  24207  vitalilem2  24213  vitalilem3  24214  vitali  24217  mbfimaopnlem  24259  mbfsup  24268  dgrval  24825  dgrcl  24830  dgrub  24831  dgrlb  24833  aannenlem3  24926  dvrelog  25228  logcn  25238  logccv  25254  ppiub  25788  lgsquadlem1  25964  lgsquadlem2  25965  addsqrexnreu  26026  addsqnreup  26027  2sqreunnlem2  26039  dirith2  26112  usgrexmpldifpr  27048  usgrexmplef  27049  disjxwwlksn  27690  disjxwwlkn  27699  nvrel  28385  phrel  28598  bnrel  28650  hlrel  28673  pjnormi  29504  lnopunilem1  29793  lnophmlem1  29799  xrge0infssd  30511  infxrge0lb  30514  infxrge0glb  30515  infxrge0gelb  30516  ssnnssfz  30536  xrge0iifiso  31288  omsf  31664  oms0  31665  omssubaddlem  31667  omssubadd  31668  oddpwdc  31722  rpsqrtcn  31974  bnj1023  32162  bnj1109  32168  erdszelem4  32554  erdszelem8  32558  gonan0  32752  supfz  33073  inffz  33074  trer  33777  fneer  33814  naim1i  33852  naim2i  33853  nmotru  33869  onpsstopbas  33891  bj-mp2c  33992  bj-mp2d  33993  bj-bijust00  34023  bj-cbvalim  34091  bj-cbvexim  34092  bj-cbvalimi  34093  bj-cbveximi  34094  iccioo01  34741  pibt2  34834  wl-equsal1i  34948  wl-sbcom2d  34962  poimirlem25  35082  poimirlem26  35083  mblfinlem1  35094  incsequz2  35187  cncfres  35203  heiborlem3  35251  diclspsn  38490  dih1dimatlem  38625  rencldnfilem  39761  pellexlem4  39773  pellexlem5  39774  ttac  39977  idomsubgmo  40142  areaquad  40166  frege102  40666  lhe4.4ex1a  41033  eel0000  41426  eel00001  41427  eel00000  41428  e000  41473  e00  41474  fzisoeu  41932  resincncf  42517  aiota0def  43651  fvmptrabdm  43849  fmtnoinf  44053  ssnn0ssfz  44751  zlmodzxzldeplem  44907