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

Theorem mp2 9
Description: A double modus ponens inference. See mp2ALT 18 for a shorter proof using two more axioms. (Contributed by NM, 5-Apr-1994.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
mp2.1  |-  ph
mp2.2  |-  ps
mp2.3  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mp2  |-  ch

Proof of Theorem mp2
StepHypRef Expression
1 mp2.2 . 2  |-  ps
2 mp2.1 . . 3  |-  ph
3 mp2.3 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3ax-mp 5 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 5 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  impbii  182  pm3.2i  443  sstri  3359  0disj  4208  disjx0  4210  relres  5177  cnvdif  5281  funopab4  5491  fun0  5511  fvsn  5929  difxp  6383  reltpos  6487  tpostpos  6502  tpos0  6512  oaabs2  6891  swoer  6936  xpider  6978  erinxp  6981  sbthcl  7232  php  7294  inf0  7579  unctb  8090  fin1a2lem12  8296  axcc2lem  8321  axcclem  8342  brdom3  8411  brdom5  8412  brdom4  8413  pwcfsdom  8463  smobeth  8466  fpwwe2lem8  8517  fpwwe2lem9  8518  fpwwe2lem12  8521  pwxpndom2  8545  pwcdandom  8547  gchac  8561  wunex3  8621  inar1  8655  gruina  8698  ltsopi  8770  recmulnq  8846  prcdnq  8875  ltrel  9145  lerel  9147  cnexALT  10613  dfle2  10745  dflt2  10746  uzrdg0i  11304  ltwefz  11308  fzennn  11312  faclbnd4lem1  11589  hashsslei  11690  isercolllem1  12463  zsum  12517  sum0  12520  xpnnenOLD  12814  znnen  12817  qnnen  12818  rpnnen  12831  ruc  12847  nthruc  12855  nthruz  12856  phicl2  13162  pwsle  13719  xpsc0  13790  xpsc1  13791  relfull  14110  relfth  14111  gicer  15068  oppglsm  15281  efgrelexlemb  15387  isunit  15767  opsrtoslem2  16550  pjpm  16940  1stcfb  17513  2ndc1stc  17519  2ndcctbss  17523  2ndcdisj2  17525  2ndcsep  17527  hmpher  17821  met1stc  18556  re2ndc  18837  iccpnfhmeo  18975  xrhmeo  18976  xrcmp  18978  xrcon  18979  dyadmbl  19497  opnmblALT  19500  vitalilem2  19506  vitalilem3  19507  vitali  19510  mbfimaopnlem  19550  mbfsup  19559  dgrval  20152  dgrcl  20157  dgrub  20158  dgrlb  20160  aannenlem3  20252  dvrelog  20533  logcn  20543  logccv  20559  ppiub  20993  lgsquadlem1  21143  lgsquadlem2  21144  dirith2  21227  usgraexmpldifpr  21424  usgraexmpl  21425  konigsberg  21714  nvrel  22086  phrel  22321  bnrel  22374  hlrel  22397  pjnormi  23228  lnopunilem1  23518  lnophmlem1  23524  ssnnssfz  24153  xrge0iifiso  24326  erdszelem4  24885  erdszelem8  24889  supfz  25204  inffz  25205  elrn3  25391  omsinds  25499  naim1i  26141  naim2i  26142  mont  26164  onpsstopbas  26185  wl-bitri  26226  mblfinlem1  26255  trer  26333  fneer  26382  incsequz2  26467  cncfres  26488  heiborlem3  26536  rencldnfilem  26895  pellexlem4  26909  pellexlem5  26910  jm2.23  27081  ttac  27121  idomsubgmo  27505  lhe4.4ex1a  27537  onfrALTlem5  28702  eel0001  28904  eel0000  28905  eel00001  28907  eel00000  28908  e000  28953  e00  28954  bnj1023  29225  bnj1109  29231  diclspsn  32066  dih1dimatlem  32201
This theorem was proved from axioms:  ax-mp 5
  Copyright terms: Public domain W3C validator