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  6164  fpmg  6793  pmresg  6795  pw2f1o  6967  pm54.43  7633  dfac2  7757  ttukeylem6  8141  gruina  8440  muleqadd  9412  divdiv1  9471  addltmul  9947  elfzm1b  10860  expp1z  11150  expm1  11151  oddvdsnn0  14859  efgi0  15029  efgi1  15030  fiinbas  16690  opnneissb  16851  fclscf  17720  blssec  17981  iimulcl  18435  itg2lr  19085  blocnilem  21382  lnopmul  22547  opsqrlem6  22725  elfzp1b  24012  fvray  24764  fvline  24767  fneref  26284  fdc  26455  rmyeq0  27040  linepmap  29964
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