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  211  imbi12i  353  pm3.2i  473  minimp-syllsimp  1619  minimp-ax2c  1621  minimp-ax2  1622  minimp-pm2.43  1623  darii  2748  barbarilem  2751  festino  2757  baroco  2759  darapti  2767  sstri  3976  0disj  5051  disjx0  5053  opthhausdorff  5400  relres  5877  cnvdif  5997  difxp  6016  funopab4  6387  fun0  6414  omsinds  7594  reltpos  7891  tpos0  7916  oaabs2  8266  swoer  8313  xpider  8362  sbthcl  8633  php  8695  elirrv  9054  inf0  9078  unctb  9621  fin1a2lem12  9827  axcc2lem  9852  axcclem  9873  brdom3  9944  brdom5  9945  brdom4  9946  pwcfsdom  9999  smobeth  10002  pwxpndom2  10081  pwdjundom  10083  gchac  10097  wunex3  10157  inar1  10191  gruina  10234  ltsopi  10304  recmulnq  10380  prcdnq  10409  ltrel  10697  lerel  10699  suprfinzcl  12091  cnexALT  12379  dfle2  12534  dflt2  12535  uzrdg0i  13321  ltwefz  13325  fzennn  13330  faclbnd4lem1  13647  hashsslei  13781  0csh0  14149  isercolllem1  15015  zsum  15069  sum0  15072  znnen  15559  qnnen  15560  rpnnen  15574  ruc  15590  nthruc  15599  nthruz  15600  phicl2  16099  relfull  17172  relfth  17173  gicer  18410  oppglsm  18761  efgrelexlemb  18870  isunit  19401  xrsnsgrp  20575  pjpm  20846  1stcfb  22047  2ndc1stc  22053  2ndcctbss  22057  2ndcdisj2  22059  2ndcsep  22061  hmpher  22386  met1stc  23125  re2ndc  23403  iccpnfhmeo  23543  xrhmeo  23544  xrcmp  23546  xrconn  23547  dyadmbl  24195  opnmblALT  24198  vitalilem2  24204  vitalilem3  24205  vitali  24208  mbfimaopnlem  24250  mbfsup  24259  dgrval  24812  dgrcl  24817  dgrub  24818  dgrlb  24820  aannenlem3  24913  dvrelog  25214  logcn  25224  logccv  25240  ppiub  25774  lgsquadlem1  25950  lgsquadlem2  25951  addsqrexnreu  26012  addsqnreup  26013  2sqreunnlem2  26025  dirith2  26098  usgrexmpldifpr  27034  usgrexmplef  27035  disjxwwlksn  27676  disjxwwlkn  27686  nvrel  28373  phrel  28586  bnrel  28638  hlrel  28661  pjnormi  29492  lnopunilem1  29781  lnophmlem1  29787  xrge0infssd  30479  infxrge0lb  30482  infxrge0glb  30483  infxrge0gelb  30484  ssnnssfz  30504  xrge0iifiso  31173  omsf  31549  oms0  31550  omssubaddlem  31552  omssubadd  31553  oddpwdc  31607  rpsqrtcn  31859  bnj1023  32047  bnj1109  32053  erdszelem4  32436  erdszelem8  32440  gonan0  32634  supfz  32955  inffz  32956  trer  33659  fneer  33696  naim1i  33734  naim2i  33735  nmotru  33751  onpsstopbas  33773  bj-mp2c  33874  bj-mp2d  33875  bj-bijust00  33905  bj-cbvalim  33973  bj-cbvexim  33974  bj-cbvalimi  33975  bj-cbveximi  33976  pibt2  34692  wl-equsal1i  34777  wl-sbcom2d  34791  poimirlem25  34911  poimirlem26  34912  mblfinlem1  34923  incsequz2  35018  cncfres  35037  heiborlem3  35085  diclspsn  38324  dih1dimatlem  38459  rencldnfilem  39410  pellexlem4  39422  pellexlem5  39423  ttac  39626  idomsubgmo  39791  areaquad  39816  frege102  40304  lhe4.4ex1a  40654  eel0000  41047  eel00001  41048  eel00000  41049  e000  41094  e00  41095  fzisoeu  41559  resincncf  42150  aiota0def  43287  fvmptrabdm  43485  fmtnoinf  43691  ssnn0ssfz  44390  zlmodzxzldeplem  44546