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

Theorem syl2anbr 482
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 475 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2br 478 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  sylancbr  670  pm2.61iineOLD  2743  reusv2  4630  tz6.12  5898  r1ord3  8261  brdom7disj  8966  brdom6disj  8967  alephadd  9009  ltresr  9571  divmuldiv  10314  fnn0ind  11041  rexanuz  13408  nprmi  14638  lsmvalx  17290  cncfval  21918  angval  23728  amgmlem  23913  sspval  26360  sshjval  27001  sshjval3  27005  hosmval  27386  hodmval  27388  hfsmval  27389  broutsideof3  30898  mptsnunlem  31704  relowlpssretop  31731
  Copyright terms: Public domain W3C validator