MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanr2 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  6330  fpmg  6975  pmresg  6977  pw2f1o  7149  pm54.43  7820  dfac2  7944  ttukeylem6  8327  gruina  8626  muleqadd  9598  divdiv1  9657  addltmul  10135  elfzm1b  11055  expp1z  11355  expm1  11356  oddvdsnn0  15109  efgi0  15279  efgi1  15280  fiinbas  16940  opnneissb  17101  fclscf  17978  blssec  18355  iimulcl  18833  itg2lr  19489  blocnilem  22153  lnopmul  23318  opsqrlem6  23496  elfzp1b  24895  fvray  25789  fvline  25792  fneref  26055  fdc  26140  rmyeq0  26709  linepmap  29889
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