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

Theorem mpanr12 692
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1  |-  ps
mpanr12.2  |-  ch
mpanr12.3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr12  |-  ( ph  ->  th )

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2  |-  ch
2 mpanr12.1 . . 3  |-  ps
3 mpanr12.3 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3mpanr1 690 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 678 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  wfisg  5418  2dom  7647  limensuci  7753  phplem4  7759  unfi  7843  fiint  7853  cdaen  8608  isfin1-3  8821  prlem934  9463  0idsr  9526  1idsr  9527  00sr  9528  addresr  9567  mulresr  9568  reclt1  10508  crne0  10609  nominpos  10856  expnass  12387  faclbnd2  12483  crim  13190  sqrlem1  13318  sqrlem7  13324  sqrt00  13339  sqreulem  13434  mulcn2  13671  ege2le3  14156  sin02gt0  14258  opoe  14773  oddprm  14777  pythagtriplem2  14779  pythagtriplem3  14780  pythagtriplem16  14792  pythagtrip  14796  pc1  14817  prmlem0  15089  acsfn0  15578  mgpress  17746  abvneg  18074  pmatcollpw3  19820  leordtval2  20240  txswaphmeo  20832  iccntr  21851  dvlipcn  22958  sinq34lt0t  23476  cosordlem  23492  efif1olem3  23505  lgamgulmlem2  23967  basellem3  24021  ppiub  24144  bposlem9  24232  lgsne0  24273  lgsdinn0  24280  chebbnd1  24322  constr1trl  25330  constr2trl  25341  usgrcyclnl2  25381  4cycl4dv  25407  2spontn0vne  25627  eupath2lem3  25719  mayete3i  27393  lnop0  27631  nmcexi  27691  nmoptrii  27759  nmopcoadji  27766  hstle1  27891  hst0  27898  strlem5  27920  jplem1  27933  cnvoprab  28320  subfacp1lem5  29919  frinsg  30495  limsucncmpi  31117  poimirlem15  31967  dvasin  32040  fdc  32086  eldioph3b  35619  sinhpcosh  40564
  Copyright terms: Public domain W3C validator