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  1622  minimp-ax2c  1624  minimp-ax2  1625  minimp-pm2.43  1626  darii  2665  barbarilem  2668  festino  2674  baroco  2676  darapti  2684  sstri  3993  0disj  5136  disjx0  5138  opthhausdorff  5522  relres  6023  cnvdif  6163  difxp  6184  funopab4  6603  fun0  6631  omsinds  7908  frxp3  8176  reltpos  8256  tpos0  8281  oaabs2  8687  swoer  8776  xpider  8828  sbthcl  9135  phpOLD  9259  elirrv  9636  unctb  10244  fin1a2lem12  10451  axcc2lem  10476  axcclem  10497  brdom3  10568  brdom5  10569  brdom4  10570  pwcfsdom  10623  smobeth  10626  pwxpndom2  10705  pwdjundom  10707  gchac  10721  wunex3  10781  inar1  10815  gruina  10858  ltsopi  10928  recmulnq  11004  prcdnq  11033  ltrel  11323  lerel  11325  suprfinzcl  12732  cnexALT  13028  dfle2  13189  dflt2  13190  uzrdg0i  14000  ltwefz  14004  fzennn  14009  faclbnd4lem1  14332  hashsslei  14465  0csh0  14831  isercolllem1  15701  zsum  15754  sum0  15757  znnen  16248  qnnen  16249  rpnnen  16263  ruc  16279  nthruc  16288  nthruz  16289  phicl2  16805  relfull  17955  relfth  17956  gicer  19295  oppglsm  19660  efgrelexlemb  19768  isunit  20373  xrsnsgrp  21420  pjpm  21728  1stcfb  23453  2ndc1stc  23459  2ndcctbss  23463  2ndcdisj2  23465  2ndcsep  23467  hmpher  23792  met1stc  24534  re2ndc  24822  iccpnfhmeo  24976  xrhmeo  24977  xrcmp  24979  xrconn  24980  dyadmbl  25635  opnmblALT  25638  vitalilem2  25644  vitalilem3  25645  vitali  25648  mbfimaopnlem  25690  mbfsup  25699  dgrval  26267  dgrcl  26272  dgrub  26273  dgrlb  26275  aannenlem3  26372  dvrelog  26679  logcn  26689  logccv  26705  ppiub  27248  lgsquadlem1  27424  lgsquadlem2  27425  addsqrexnreu  27486  addsqnreup  27487  2sqreunnlem2  27499  dirith2  27572  madefi  27950  usgrexmpldifpr  29275  usgrexmplef  29276  disjxwwlksn  29924  disjxwwlkn  29933  nvrel  30621  phrel  30834  bnrel  30886  hlrel  30909  pjnormi  31740  lnopunilem1  32029  lnophmlem1  32035  xrge0infssd  32765  infxrge0lb  32768  infxrge0glb  32769  infxrge0gelb  32770  ssnnssfz  32789  xrge0iifiso  33934  omsf  34298  oms0  34299  omssubaddlem  34301  omssubadd  34302  oddpwdc  34356  rpsqrtcn  34608  bnj1023  34794  bnj1109  34800  erdszelem4  35199  erdszelem8  35203  gonan0  35397  2thALT  35689  supfz  35729  inffz  35730  trer  36317  fneer  36354  naim1i  36392  naim2i  36393  nmotru  36409  onpsstopbas  36431  bj-mp2c  36541  bj-mp2d  36542  bj-bijust00  36578  bj-cbvalim  36646  bj-cbvexim  36647  bj-cbvalimi  36648  bj-cbveximi  36649  iccioo01  37328  pibt2  37418  wl-equsal1i  37545  wl-sbcom2d  37562  poimirlem25  37652  poimirlem26  37653  mblfinlem1  37664  incsequz2  37756  cncfres  37772  heiborlem3  37820  diclspsn  41196  dih1dimatlem  41331  rencldnfilem  42831  pellexlem4  42843  pellexlem5  42844  ttac  43048  idomsubgmo  43205  areaquad  43228  frege102  43978  lhe4.4ex1a  44348  eel0000  44740  eel00001  44741  eel00000  44742  e000  44787  e00  44788  wffr  44978  modelaxreplem1  44995  fzisoeu  45312  resincncf  45890  aiota0def  47108  fvmptrabdm  47305  fmtnoinf  47523  gricrel  47888  grlicrel  47966  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  ssnn0ssfz  48265  zlmodzxzldeplem  48415  tposideq  48788