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

Theorem syl2anbr 466
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 459 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2br 462 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  sylancbr  647  reusv2  4540  tz6.12  5545  r1ord3  7454  brdom7disj  8156  brdom6disj  8157  alephadd  8199  ltresr  8762  divmuldiv  9460  fnn0ind  10111  rexanuz  11829  nprmi  12773  lsmvalx  14950  cncfval  18392  angval  20099  amgmlem  20284  sspval  21299  sshjval  21929  sshjval3  21933  hosmval  22315  hodmval  22317  hfsmval  22318  pm2.61iine  24081  broutsideof3  24749  cptwff  25107
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