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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  impbii  212  imbi12i  353  pm3.2i  476  minimp-syllsimp  1654  minimp-ax2c  1656  minimp-ax2  1657  minimp-pm2.43  1658  darii  2689  barbarilem  2692  festino  2698  baroco  2700  darapti  2708  sstri  3917  0disj  5095  disjx0  5097  opthhausdorff  5489  relres  5995  cnvdif  6133  difxp  6154  funopab4  6577  fun0  6605  omsinds  7898  frxp3  8170  reltpos  8251  tpos0  8276  oaabs2  8661  swoer  8752  xpider  8812  sbthcl  9121  elirrvOLDOLD  9596  unctb  10285  fin1a2lem12  10492  axcc2lem  10517  axcclem  10538  brdom3  10610  brdom5  10611  brdom4  10612  pwcfsdom  10671  smobeth  10674  pwxpndom2  10753  pwdjundom  10755  gchac  10769  wunex3  10829  inar1  10863  gruina  10906  ltsopi  10976  recmulnq  11052  prcdnq  11081  ltrel  11374  lerel  11376  suprfinzcl  12816  cnexALT  13117  dfle2  13279  dflt2  13280  uzrdg0i  14105  ltwefz  14109  fzennn  14114  faclbnd4lem1  14440  hashsslei  14574  0csh0  14948  isercolllem1  15837  zsum  15889  sum0  15892  znnen  16385  qnnen  16386  rpnnen  16400  ruc  16416  nthruc  16425  nthruz  16426  phicl2  16950  relfull  18090  relfth  18091  gicer  19496  oppglsm  19861  efgrelexlemb  19969  isunit  20608  ricrel  20749  xrsnsgrp  21719  pjpm  22019  1stcfb  23768  2ndc1stc  23774  2ndcctbss  23779  2ndcdisj2  23781  2ndcsep  23783  hmpher  24108  met1stc  24845  re2ndc  25125  iccpnfhmeo  25271  xrhmeo  25272  xrcmp  25274  xrconn  25275  dyadmbl  25926  opnmblALT  25929  vitalilem2  25935  vitalilem3  25936  vitali  25939  mbfimaopnlem  25981  mbfsup  25990  dgrval  26552  dgrcl  26557  dgrub  26558  dgrlb  26560  aannenlem3  26662  dvrelog  26970  logcn  26980  logccv  26996  ppiub  27536  lgsquadlem1  27712  lgsquadlem2  27713  addsqrexnreu  27774  addsqnreup  27775  2sqreunnlem2  27787  dirith2  27860  bdayfinbndlem1  28858  usgrexmpldifpr  29844  usgrexmplef  29845  disjxwwlksn  30498  disjxwwlkn  30507  nvrel  31209  phrel  31422  bnrel  31474  hlrel  31497  pjnormi  32328  lnopunilem1  32617  lnophmlem1  32623  xrge0infssd  33399  infxrge0lb  33402  infxrge0glb  33403  infxrge0gelb  33404  ssnnssfz  33425  xrge0iifiso  34613  omsf  34974  oms0  34975  omssubaddlem  34977  omssubadd  34978  oddpwdc  35032  rpsqrtcn  35268  bnj1023  35457  bnj1109  35463  erdszelem4  36045  erdszelem8  36049  gonan0  36243  2thALT  36535  onprcr  36548  supfz  36586  inffz  36587  trer  37196  fneer  37233  naim1i  37271  naim2i  37272  nmotru  37288  onpsstopbas  37310  bj-mp2c  37498  bj-mp2d  37499  bj-bijust00  37539  bj-almp  37573  bj-axseprep  38082  iccioo01  38343  pibt2  38433  wl-equsal1i  38569  wl-sbcom2d  38586  poimirlem25  38656  poimirlem26  38657  mblfinlem1  38668  incsequz2  38776  cncfres  38792  heiborlem3  38840  diclspsn  42344  dih1dimatlem  42479  rencldnfilem  43920  pellexlem4  43932  pellexlem5  43933  ttac  44136  idomsubgmo  44288  areaquad  44311  frege102  45058  lhe4.4ex1a  45406  eel0000  45795  eel00001  45796  eel00000  45797  e000  45842  e00  45843  wffr  46044  modelaxreplem1  46061  nregmodellem  46099  fzisoeu  46409  resincncf  46978  numtowerdt  48009  aiota0def  48259  fvmptrabdm  48456  fmtnoinf  48714  gricrel  49110  grlicrel  49197  usgrexmpl1lem  49212  usgrexmpl2lem  49217  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  gpgprismgr4cycllem2  49287  gpg5ngric  49319  ssnn0ssfz  49554  zlmodzxzldeplem  49703  tposideq  50094