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

Theorem mpanr2 666
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 527 . 2  |-  ( ps 
->  ( ps  /\  ch ) )
3 mpanr2.2 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3sylan2 461 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  op1steq  6383  fpmg  7031  pmresg  7033  pw2f1o  7205  pm54.43  7879  dfac2  8003  ttukeylem6  8386  gruina  8685  muleqadd  9658  divdiv1  9717  addltmul  10195  elfzm1b  11117  expp1z  11420  expm1  11421  oddvdsnn0  15174  efgi0  15344  efgi1  15345  fiinbas  17009  opnneissb  17170  fclscf  18049  blssec  18457  iimulcl  18954  itg2lr  19614  blocnilem  22297  lnopmul  23462  opsqrlem6  23640  elfzp1b  25108  fvray  26067  fvline  26070  fneref  26355  fdc  26440  rmyeq0  27009  linepmap  30509
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 178  df-an 361
  Copyright terms: Public domain W3C validator