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

Theorem syl6bbr 197
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 131 . 2  |-  ( ch  <->  th )
41, 3syl6bb 195 1  |-  ( ph  ->  ( ps  <->  th )
)
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:  3bitr4g  222  bibi2i  226  equsalh  1705  eueq3dc  2861  sbcel12g  3021  sbceqg  3022  sbcnel12g  3023  reldisj  3418  r19.3rm  3455  eldifpr  3558  eldiftp  3576  rabxp  4583  elrng  4737  iss  4872  eliniseg  4916  fcnvres  5313  dffv3g  5424  funimass4  5479  fndmdif  5532  fneqeql  5535  funimass3  5543  elrnrexdmb  5567  dff4im  5573  fconst4m  5647  elunirn  5674  riota1  5755  riota2df  5757  f1ocnvfv3  5770  eqfnov  5884  caoftrn  6014  mpoxopovel  6145  rntpos  6161  ordgt0ge1  6339  iinerm  6508  erinxp  6510  qliftfun  6518  mapdm0  6564  elfi2  6867  fifo  6875  inl11  6957  ctssdccl  7003  isomnimap  7016  ismkvmap  7035  iswomnimap  7047  omniwomnimkv  7048  pr2nelem  7063  indpi  7173  genpdflem  7338  genpdisj  7354  genpassl  7355  genpassu  7356  ltnqpri  7425  ltpopr  7426  ltexprlemm  7431  ltexprlemdisj  7437  ltexprlemloc  7438  ltrennb  7685  letri3  7868  letr  7870  ltneg  8247  leneg  8250  reapltxor  8374  apsym  8391  suprnubex  8734  suprleubex  8735  elnnnn0  9043  zrevaddcl  9127  znnsub  9128  znn0sub  9142  prime  9173  eluz2  9355  eluz2b1  9421  nn01to3  9435  qrevaddcl  9462  xrletri3  9617  xrletr  9620  iccid  9737  elicopnf  9781  fzsplit2  9860  fzsn  9876  fzpr  9887  uzsplit  9902  fvinim0ffz  10048  lt2sqi  10410  le2sqi  10411  abs00ap  10865  iooinsup  11077  mertenslem2  11336  gcddiv  11741  algcvgblem  11764  isprm3  11833  eltg2b  12260  discld  12342  opnssneib  12362  restbasg  12374  ssidcn  12416  cnptoprest2  12446  lmss  12452  txrest  12482  txlm  12485  imasnopn  12505  bldisj  12607  xmeter  12642  bl2ioo  12748  limcdifap  12837  bj-sseq  13168  nnti  13360  pw1nct  13369
  Copyright terms: Public domain W3C validator