MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anbr Structured version   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  4721  tz6.12  5740  r1ord3  7700  brdom7disj  8401  brdom6disj  8402  alephadd  8444  ltresr  9007  divmuldiv  9706  fnn0ind  10361  rexanuz  12141  nprmi  13086  lsmvalx  15265  cncfval  18910  angval  20635  amgmlem  20820  sspval  22214  sshjval  22844  sshjval3  22848  hosmval  23230  hodmval  23232  hfsmval  23233  pm2.61iine  25178  broutsideof3  26052
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