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

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

Proof of Theorem syl6bb
StepHypRef Expression
1 syl6bb.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6bb.2 . . 3  |-  ( ch  <->  th )
32a1i 9 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 181 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:  syl6rbb  190  syl6bbr  191  3bitr3g  215  bibi2i  220  ibibr  239  imandc  797  pm5.75  880  xordidc  1306  19.17  1464  alexdc  1526  nf4dc  1576  abeq2d  2166  cbvralf  2544  cbvrexf  2545  cbvreu  2548  cbvrab  2572  ceqsralt  2598  ralab2  2728  rexab2  2730  euxfr2dc  2749  reu7  2759  reu8  2760  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  ralss  3034  rexss  3035  prssg  3549  2ralunsn  3597  eluniab  3620  elintab  3654  dfiun2g  3717  dfiin2g  3718  cbvopab1  3858  cbvmpt  3879  axsep2  3904  bnd2  3954  opeqsn  4017  reusv3  4220  tfisi  4338  opeliunxp  4423  eliunxp  4503  relop  4514  eldm2g  4559  reldm0  4581  relrn0  4622  xpmlem  4772  elxp5  4837  cnvpom  4888  cbviota  4900  iota1  4909  sniota  4922  fncnv  4993  fnres  5043  brprcneu  5199  fnopfvb  5243  fvelrnb  5249  fvelimab  5257  fvopab3g  5273  eqfnfv3  5295  eqfnfv2f  5297  fvreseq  5299  fnreseql  5305  rexsupp  5319  respreima  5323  rexrn  5332  ralrn  5333  f1ompt  5348  fsn  5363  fconstfvm  5407  fconst3m  5408  fconst4m  5409  rexima  5422  ralima  5423  dff13  5435  foeqcnvco  5458  fliftfun  5464  isocnv  5479  isoini  5485  f1oiso  5493  cbvriota  5506  eusvobj2  5526  oprabid  5565  eloprabga  5619  resoprab  5625  eqfnov  5635  eqfnov2  5636  ov6g  5666  funimassov  5678  ovelimab  5679  caovord2  5701  releldm2  5839  dfoprab4  5846  xporderlem  5880  poxp  5881  f1od2  5884  mpt2xopovel  5887  brtpos2  5897  brtpos0  5898  rntpos  5903  dftpos3  5908  tpostpos  5910  tpossym  5922  tposoprab  5926  frecsuclem3  6021  erth2  6182  qliftfun  6219  erovlem  6229  ecopovsym  6233  ecopovsymg  6236  th3qlem1  6239  dom2lem  6283  xpdom2  6336  ssfiexmid  6367  diffitest  6375  ac6sfi  6383  isoti  6411  ltexpi  6493  ordpipqqs  6530  ltexnqq  6564  enq0enq  6587  enq0sym  6588  enq0tr  6590  nqnq0pi  6594  genipv  6665  genprndl  6677  genprndu  6678  genpdisj  6679  genpassl  6680  genpassu  6681  addcomprg  6734  mulcomprg  6736  ltnqpr  6749  ltnqpri  6750  ltexprlemm  6756  ltexprlemdisj  6762  ltsrprg  6890  mulgt0sr  6920  elreal2  6965  ltresr  6973  ltresr2  6974  axprecex  7012  axpre-ltadd  7018  axpre-mulgt0  7019  axpre-mulext  7020  subcan2  7299  negcon1  7326  negcon2  7327  lt0neg1  7537  lt0neg2  7538  le0neg1  7539  le0neg2  7540  reapirr  7642  reapmul1  7660  reapneg  7662  remulext1  7664  apti  7687  negap0  7694  divmulap2  7729  reclt1  7937  recgt1  7938  addltmul  8218  elznn0  8317  zapne  8373  zltlen  8377  nn0lt10b  8379  nn0lt2  8380  eluz1  8573  raluz  8617  rexuz  8619  qltlen  8672  cnref1o  8680  rpnegap  8713  ltxr  8796  xlt0neg1  8852  xlt0neg2  8853  xle0neg1  8854  xle0neg2  8855  elixx1  8867  elixx3g  8871  elioo2  8891  icc0r  8896  elicc4  8910  elioopnf  8937  elioomnf  8938  iooneg  8957  iccneg  8958  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  iccf1o  8973  elfz1  8981  0fz1  9011  fzpr  9041  fzdifsuc  9045  uzsplit  9056  elfzm1b  9062  elfzp12  9063  fznn0  9076  flqeqceilz  9268  zmodid2  9302  expap0  9450  bernneq  9537  sqrtmsq2i  9962  clim0  10037  climrecvg1n  10098  dvdsval2  10111  odd2np1lem  10183  even2n  10185  divalgb  10237  divalgmod  10239  sqrt2irr  10251
  Copyright terms: Public domain W3C validator