MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mp2.2 . 2 𝜓
2 mp2.1 . . 3 𝜑
3 mp2.3 . . 3 (𝜑 → (𝜓𝜒))
42, 3ax-mp 5 . 2 (𝜓𝜒)
51, 4ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  impbii  199  imbi12i  339  pm3.2i  447  minimp-syllsimp  1709  minimp-ax2c  1711  minimp-ax2  1712  minimp-pm2.43  1713  sbcom2  2593  sstri  3761  0disj  4779  disjx0  4781  opthhausdorff  5110  relres  5567  cnvdif  5680  difxp  5699  funopab4  6068  fun0  6094  fvsn  6590  omsinds  7231  reltpos  7509  tpostpos  7524  tpos0  7534  oaabs2  7879  swoer  7926  xpider  7970  erinxp  7973  sbthcl  8238  php  8300  elirrv  8657  inf0  8682  unctb  9229  fin1a2lem12  9435  axcc2lem  9460  axcclem  9481  brdom3  9552  brdom5  9553  brdom4  9554  pwcfsdom  9607  smobeth  9610  fpwwe2lem8  9661  fpwwe2lem9  9662  fpwwe2lem12  9665  pwxpndom2  9689  pwcdandom  9691  gchac  9705  wunex3  9765  inar1  9799  gruina  9842  ltsopi  9912  recmulnq  9988  prcdnq  10017  ltrel  10302  lerel  10304  suprfinzcl  11694  cnexALT  12031  dfle2  12185  dflt2  12186  uzrdg0i  12966  ltwefz  12970  fzennn  12975  faclbnd4lem1  13284  hashsslei  13415  0csh0  13748  isercolllem1  14603  zsum  14657  sum0  14660  znnen  15147  qnnen  15148  rpnnen  15162  ruc  15178  nthruc  15187  nthruz  15188  phicl2  15680  pwsle  16360  xpsc0  16428  xpsc1  16429  relfull  16775  relfth  16776  gicer  17926  oppglsm  18264  efgrelexlemb  18370  isunit  18865  opsrtoslem2  19700  xrsnsgrp  19997  pjpm  20269  1stcfb  21469  2ndc1stc  21475  2ndcctbss  21479  2ndcdisj2  21481  2ndcsep  21483  hmpher  21808  met1stc  22546  re2ndc  22824  iccpnfhmeo  22964  xrhmeo  22965  xrcmp  22967  xrconn  22968  dyadmbl  23588  opnmblALT  23591  vitalilem2  23597  vitalilem3  23598  vitali  23601  mbfimaopnlem  23642  mbfsup  23651  dgrval  24204  dgrcl  24209  dgrub  24210  dgrlb  24212  aannenlem3  24305  dvrelog  24604  logcn  24614  logccv  24630  logblog  24751  ppiub  25150  lgsquadlem1  25326  lgsquadlem2  25327  dirith2  25438  usgrexmpldifpr  26373  usgrexmplef  26374  disjxwwlksn  27048  disjxwwlkn  27058  nvrel  27797  phrel  28010  bnrel  28063  hlrel  28086  pjnormi  28920  lnopunilem1  29209  lnophmlem1  29215  xrge0infssd  29866  infxrge0lb  29869  infxrge0glb  29870  infxrge0gelb  29871  ssnnssfz  29889  xrge0iifiso  30321  omsf  30698  oms0  30699  omssubaddlem  30701  omssubadd  30702  oddpwdc  30756  rpsqrtcn  31011  bnj1023  31189  bnj1109  31195  erdszelem4  31514  erdszelem8  31518  supfz  31951  inffz  31952  inffzOLD  31953  elrn3  31990  trer  32647  fneer  32685  naim1i  32723  naim2i  32724  mont  32745  onpsstopbas  32766  bj-mp2c  32868  bj-mp2d  32869  bj-currypeirce  32881  wl-equsal1i  33664  wl-sbcom2d  33678  poimirlem25  33767  poimirlem26  33768  mblfinlem1  33779  incsequz2  33877  cncfres  33896  heiborlem3  33944  diclspsn  37004  dih1dimatlem  37139  rencldnfilem  37910  pellexlem4  37922  pellexlem5  37923  ttac  38129  idomsubgmo  38302  areaquad  38328  frege102  38785  lhe4.4ex1a  39054  eel0001  39470  eel0000  39471  eel00001  39473  eel00000  39474  e000  39519  e00  39520  fzisoeu  40031  resincncf  40606  fvmptrabdm  41835  fmtnoinf  41976  ssnn0ssfz  42655  zlmodzxzldeplem  42815
  Copyright terms: Public domain W3C validator