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  2771  reusv2  4596  tz6.12  5806  r1ord3  8090  brdom7disj  8799  brdom6disj  8800  alephadd  8842  ltresr  9408  divmuldiv  10132  fnn0ind  10842  rexanuz  12935  nprmi  13880  lsmvalx  16242  cncfval  20580  angval  22313  amgmlem  22499  sspval  24256  sshjval  24888  sshjval3  24892  hosmval  25274  hodmval  25276  hfsmval  25277  broutsideof3  28291
  Copyright terms: Public domain W3C validator