ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6rbbr Unicode version

Theorem syl6rbbr 192
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6rbbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6rbbr  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 127 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 190 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imimorbdc  806  baib  839  pm5.6dc  846  xornbidc  1298  mo2dc  1971  reu8  2760  sbc6g  2811  r19.28m  3339  r19.45mv  3343  r19.27m  3344  ralsnsg  3435  ralsns  3436  rexsnsOLD  3438  iunconstm  3693  iinconstm  3694  unisucg  4179  funssres  4970  fncnv  4993  dff1o5  5163  funimass4  5252  fneqeql2  5304  fnniniseg2  5318  rexsupp  5319  unpreima  5320  dffo3  5342  funfvima  5418  dff13  5435  f1eqcocnv  5459  fliftf  5467  isocnv2  5480  eloprabga  5619  mpt22eqb  5638  opabex3d  5776  opabex3  5777  elxp6  5824  elxp7  5825  genpdflem  6663  ltnqpr  6749  ltexprlemloc  6763  xrlenlt  7143  negcon2  7327  elznn  8318  zq  8658  rpnegap  8713  modqmuladdnn0  9318  shftdm  9651  rexfiuz  9816  rexanuz2  9818  odd2np1  10184  divalgb  10237
  Copyright terms: Public domain W3C validator