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  5908  op1steq  6723  fpmg  7343  pmresg  7345  pw2f1o  7521  pm54.43  8276  dfac2  8406  ttukeylem6  8789  gruina  9091  muleqadd  10086  divdiv1  10148  addltmul  10666  elfzp1b  11649  elfzm1b  11650  expp1z  12024  expm1  12025  oddvdsnn0  16163  efgi0  16333  efgi1  16334  fiinbas  18684  opnneissb  18845  fclscf  19725  blssec  20137  iimulcl  20636  itg2lr  21336  blocnilem  24351  lnopmul  25518  opsqrlem6  25696  gsumle  26386  gsumvsca1  26391  gsumvsca2  26392  fvray  28311  fvline  28314  fneref  28699  fdc  28784  rmyeq0  29439  linepmap  33738
  Copyright terms: Public domain W3C validator