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

Theorem syl2anbr 480
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 473 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2br 476 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    /\ 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 187  df-an 371
This theorem is referenced by:  sylancbr  666  pm2.61iineOLD  2728  reusv2  4602  tz6.12  5868  r1ord3  8234  brdom7disj  8943  brdom6disj  8944  alephadd  8986  ltresr  9549  divmuldiv  10287  fnn0ind  11004  rexanuz  13329  nprmi  14443  lsmvalx  16985  cncfval  21686  angval  23462  amgmlem  23647  sspval  26063  sshjval  26695  sshjval3  26699  hosmval  27080  hodmval  27082  hfsmval  27083  broutsideof3  30477  mptsnunlem  31267  relowlpssretop  31294
  Copyright terms: Public domain W3C validator