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

Theorem mpanr2 684
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 542 . 2  |-  ( ps 
->  ( ps  /\  ch ) )
3 mpanr2.2 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3sylan2 474 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  fvreseq1  5980  op1steq  6823  fpmg  7441  pmresg  7443  pw2f1o  7619  pm54.43  8377  dfac2  8507  ttukeylem6  8890  gruina  9192  muleqadd  10189  divdiv1  10251  addltmul  10770  elfzp1b  11751  elfzm1b  11752  expp1z  12178  expm1  12179  oddvdsnn0  16364  efgi0  16534  efgi1  16535  fiinbas  19220  opnneissb  19381  fclscf  20261  blssec  20673  iimulcl  21172  itg2lr  21872  blocnilem  25395  lnopmul  26562  opsqrlem6  26740  gsumle  27433  gsumvsca1  27436  gsumvsca2  27437  fvray  29368  fvline  29371  fneref  29756  fdc  29841  rmyeq0  30495  linepmap  34571
  Copyright terms: Public domain W3C validator