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  208  imbi12i  350  pm3.2i  470  minimp-syllsimp  1626  minimp-ax2c  1628  minimp-ax2  1629  minimp-pm2.43  1630  darii  2666  barbarilem  2669  festino  2675  baroco  2677  darapti  2685  sstri  3926  0disj  5062  disjx0  5064  opthhausdorff  5425  relres  5909  cnvdif  6036  difxp  6056  funopab4  6455  fun0  6483  omsinds  7708  omsindsOLD  7709  reltpos  8018  tpos0  8043  oaabs2  8439  swoer  8486  xpider  8535  sbthcl  8835  php  8897  elirrv  9285  unctb  9892  fin1a2lem12  10098  axcc2lem  10123  axcclem  10144  brdom3  10215  brdom5  10216  brdom4  10217  pwcfsdom  10270  smobeth  10273  pwxpndom2  10352  pwdjundom  10354  gchac  10368  wunex3  10428  inar1  10462  gruina  10505  ltsopi  10575  recmulnq  10651  prcdnq  10680  ltrel  10968  lerel  10970  suprfinzcl  12365  cnexALT  12655  dfle2  12810  dflt2  12811  uzrdg0i  13607  ltwefz  13611  fzennn  13616  faclbnd4lem1  13935  hashsslei  14069  0csh0  14434  isercolllem1  15304  zsum  15358  sum0  15361  znnen  15849  qnnen  15850  rpnnen  15864  ruc  15880  nthruc  15889  nthruz  15890  phicl2  16397  relfull  17540  relfth  17541  gicer  18807  oppglsm  19162  efgrelexlemb  19271  isunit  19814  xrsnsgrp  20546  pjpm  20825  1stcfb  22504  2ndc1stc  22510  2ndcctbss  22514  2ndcdisj2  22516  2ndcsep  22518  hmpher  22843  met1stc  23583  re2ndc  23870  iccpnfhmeo  24014  xrhmeo  24015  xrcmp  24017  xrconn  24018  dyadmbl  24669  opnmblALT  24672  vitalilem2  24678  vitalilem3  24679  vitali  24682  mbfimaopnlem  24724  mbfsup  24733  dgrval  25294  dgrcl  25299  dgrub  25300  dgrlb  25302  aannenlem3  25395  dvrelog  25697  logcn  25707  logccv  25723  ppiub  26257  lgsquadlem1  26433  lgsquadlem2  26434  addsqrexnreu  26495  addsqnreup  26496  2sqreunnlem2  26508  dirith2  26581  usgrexmpldifpr  27528  usgrexmplef  27529  disjxwwlksn  28170  disjxwwlkn  28179  nvrel  28865  phrel  29078  bnrel  29130  hlrel  29153  pjnormi  29984  lnopunilem1  30273  lnophmlem1  30279  xrge0infssd  30986  infxrge0lb  30989  infxrge0glb  30990  infxrge0gelb  30991  ssnnssfz  31010  xrge0iifiso  31787  omsf  32163  oms0  32164  omssubaddlem  32166  omssubadd  32167  oddpwdc  32221  rpsqrtcn  32473  bnj1023  32660  bnj1109  32666  erdszelem4  33056  erdszelem8  33060  gonan0  33254  supfz  33600  inffz  33601  trer  34432  fneer  34469  naim1i  34507  naim2i  34508  nmotru  34524  onpsstopbas  34546  bj-mp2c  34647  bj-mp2d  34648  bj-bijust00  34685  bj-cbvalim  34753  bj-cbvexim  34754  bj-cbvalimi  34755  bj-cbveximi  34756  iccioo01  35425  pibt2  35515  wl-equsal1i  35629  wl-sbcom2d  35643  poimirlem25  35729  poimirlem26  35730  mblfinlem1  35741  incsequz2  35834  cncfres  35850  heiborlem3  35898  diclspsn  39135  dih1dimatlem  39270  rencldnfilem  40558  pellexlem4  40570  pellexlem5  40571  ttac  40774  idomsubgmo  40939  areaquad  40963  frege102  41462  lhe4.4ex1a  41836  eel0000  42229  eel00001  42230  eel00000  42231  e000  42276  e00  42277  fzisoeu  42729  resincncf  43306  aiota0def  44475  fvmptrabdm  44672  fmtnoinf  44876  ssnn0ssfz  45573  zlmodzxzldeplem  45727