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

Theorem syl6bbr 191
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6bbr  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6bbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 127 . 2  |-  ( ch  <->  th )
41, 3syl6bb 189 1  |-  ( ph  ->  ( ps  <->  th )
)
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:  3bitr4g  216  bibi2i  220  equsalh  1630  eueq3dc  2738  sbcel12g  2893  sbceqg  2894  sbcnel12g  2895  reldisj  3299  r19.3rm  3338  rabxp  4408  elrng  4554  iss  4682  eliniseg  4723  fcnvres  5101  dffv3g  5202  funimass4  5252  fndmdif  5300  fneqeql  5303  funimass3  5311  elrnrexdmb  5335  dff4im  5341  fconst4m  5409  elunirn  5433  riota1  5514  riota2df  5516  f1ocnvfv3  5529  eqfnov  5635  caoftrn  5764  mpt2xopovel  5887  rntpos  5903  ordgt0ge1  6049  iinerm  6209  erinxp  6211  qliftfun  6219  indpi  6498  genpdflem  6663  genpdisj  6679  genpassl  6680  genpassu  6681  ltnqpri  6750  ltpopr  6751  ltexprlemm  6756  ltexprlemdisj  6762  ltexprlemloc  6763  ltrennb  6988  letri3  7158  letr  7160  ltneg  7531  leneg  7534  reapltxor  7654  apsym  7671  elnnnn0  8282  zrevaddcl  8352  znnsub  8353  znn0sub  8367  prime  8396  eluz2  8575  eluz2b1  8635  nn01to3  8649  qrevaddcl  8676  xrletri3  8822  xrletr  8825  iccid  8895  elicopnf  8939  fzsplit2  9016  fzsn  9031  fzpr  9041  uzsplit  9056  fvinim0ffz  9198  lt2sqi  9507  le2sqi  9508  abs00ap  9889  algcvgblem  10271  bj-sseq  10318
  Copyright terms: Public domain W3C validator