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

Theorem syl6rbbr 198
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 131 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 196 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imimorbdc  866  baib  889  pm5.6dc  896  xornbidc  1354  mo2dc  2032  reu8  2853  sbc6g  2906  dfss4st  3279  r19.28m  3422  r19.45mv  3426  r19.44mv  3427  r19.27m  3428  ralsnsg  3531  ralsns  3532  iunconstm  3791  iinconstm  3792  exmidsssnc  4096  unisucg  4306  relsng  4612  funssres  5135  fncnv  5159  dff1o5  5344  funimass4  5440  fneqeql2  5497  fnniniseg2  5511  rexsupp  5512  unpreima  5513  dffo3  5535  funfvima  5617  dff13  5637  f1eqcocnv  5660  fliftf  5668  isocnv2  5681  eloprabga  5826  mpo2eqb  5848  opabex3d  5987  opabex3  5988  elxp6  6035  elxp7  6036  sbthlemi5  6817  sbthlemi6  6818  genpdflem  7283  ltnqpr  7369  ltexprlemloc  7383  xrlenlt  7797  negcon2  7983  dfinfre  8682  sup3exmid  8683  elznn  9038  zq  9386  rpnegap  9442  modqmuladdnn0  10109  shftdm  10562  rexfiuz  10729  rexanuz2  10731  sumsplitdc  11169  fsum2dlemstep  11171  odd2np1  11497  divalgb  11549  infssuzex  11569  isprm4  11727  ctiunctlemudc  11877  tx1cn  12365  tx2cn  12366  cnbl0  12630  cnblcld  12631  reopnap  12634  pilem1  12787  sinq34lt0t  12839
  Copyright terms: Public domain W3C validator