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  4556  tz6.12  5561  r1ord3  7470  brdom7disj  8172  brdom6disj  8173  alephadd  8215  ltresr  8778  divmuldiv  9476  fnn0ind  10127  rexanuz  11845  nprmi  12789  lsmvalx  14966  cncfval  18408  angval  20115  amgmlem  20300  sspval  21315  sshjval  21945  sshjval3  21949  hosmval  22331  hodmval  22333  hfsmval  22334  pm2.61iine  24096  broutsideof3  24821  cptwff  25210
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