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 184    /\ 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 185  df-an 371
This theorem is referenced by:  sylancbr  666  pm2.61iineOLD  2790  reusv2  4653  tz6.12  5881  r1ord3  8196  brdom7disj  8905  brdom6disj  8906  alephadd  8948  ltresr  9513  divmuldiv  10240  fnn0ind  10956  rexanuz  13137  nprmi  14087  lsmvalx  16455  cncfval  21127  angval  22861  amgmlem  23047  sspval  25312  sshjval  25944  sshjval3  25948  hosmval  26330  hodmval  26332  hfsmval  26333  broutsideof3  29353
  Copyright terms: Public domain W3C validator