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

Theorem mpanr2 665
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanr2.1  |-  ch
mpanr2.2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr2  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mpanr2
StepHypRef Expression
1 mpanr2.1 . . 3  |-  ch
21jctr 526 . 2  |-  ( ps 
->  ( ps  /\  ch ) )
3 mpanr2.2 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3sylan2 460 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  op1steq  6180  fpmg  6809  pmresg  6811  pw2f1o  6983  pm54.43  7649  dfac2  7773  ttukeylem6  8157  gruina  8456  muleqadd  9428  divdiv1  9487  addltmul  9963  elfzm1b  10876  expp1z  11166  expm1  11167  oddvdsnn0  14875  efgi0  15045  efgi1  15046  fiinbas  16706  opnneissb  16867  fclscf  17736  blssec  17997  iimulcl  18451  itg2lr  19101  blocnilem  21398  lnopmul  22563  opsqrlem6  22741  elfzp1b  24027  fvray  24836  fvline  24839  fneref  26387  fdc  26558  rmyeq0  27143  linepmap  30586
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator