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

Theorem syl2anbr 467
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anbr.1  |-  ( ps  <->  ph )
syl2anbr.2  |-  ( ch  <->  ta )
syl2anbr.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anbr  |-  ( (
ph  /\  ta )  ->  th )

Proof of Theorem syl2anbr
StepHypRef Expression
1 syl2anbr.2 . 2  |-  ( ch  <->  ta )
2 syl2anbr.1 . . 3  |-  ( ps  <->  ph )
3 syl2anbr.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylanbr 460 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2br 463 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  sylancbr  648  reusv2  4669  tz6.12  5688  r1ord3  7641  brdom7disj  8342  brdom6disj  8343  alephadd  8385  ltresr  8948  divmuldiv  9646  fnn0ind  10301  rexanuz  12076  nprmi  13021  lsmvalx  15200  cncfval  18789  angval  20510  amgmlem  20695  sspval  22070  sshjval  22700  sshjval3  22704  hosmval  23086  hodmval  23088  hfsmval  23089  pm2.61iine  24965  broutsideof3  25774
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