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

Theorem syl6rbbr 197
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 130 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 195 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imimorbdc  833  baib  866  pm5.6dc  873  xornbidc  1327  mo2dc  2003  reu8  2809  sbc6g  2862  dfss4st  3230  r19.28m  3367  r19.45mv  3371  r19.44mv  3372  r19.27m  3373  ralsnsg  3475  ralsns  3476  iunconstm  3733  iinconstm  3734  unisucg  4232  relsng  4529  funssres  5042  fncnv  5066  dff1o5  5246  funimass4  5339  fneqeql2  5392  fnniniseg2  5406  rexsupp  5407  unpreima  5408  dffo3  5430  funfvima  5508  dff13  5529  f1eqcocnv  5552  fliftf  5560  isocnv2  5573  eloprabga  5717  mpt22eqb  5736  opabex3d  5874  opabex3  5875  elxp6  5922  elxp7  5923  sbthlemi5  6649  sbthlemi6  6650  genpdflem  7045  ltnqpr  7131  ltexprlemloc  7145  xrlenlt  7530  negcon2  7714  dfinfre  8389  elznn  8736  zq  9080  rpnegap  9135  modqmuladdnn0  9740  shftdm  10221  rexfiuz  10387  rexanuz2  10389  sumsplitdc  10789  fsum2dlemstep  10791  odd2np1  10966  divalgb  11018  infssuzex  11038  isprm4  11194
  Copyright terms: Public domain W3C validator