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

Theorem syl6bb 195
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 187 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl6rbb  196  syl6bbr  197  3bitr3g  221  bibi2i  226  ibibr  245  imanst  780  imandc  825  pm5.75  909  xordidc  1336  19.17  1494  alexdc  1556  nf4dc  1606  abeq2d  2201  cbvralf  2587  cbvrexf  2588  cbvreu  2591  cbvrab  2620  ceqsralt  2649  ralab2  2782  rexab2  2784  euxfr2dc  2803  reu7  2813  reu8  2814  cbvralcsf  2993  cbvrexcsf  2994  cbvreucsf  2995  cbvrabcsf  2996  ralss  3090  rexss  3091  prssg  3602  2ralunsn  3650  eluniab  3673  elintab  3707  dfiun2g  3770  dfiin2g  3771  cbvopab1  3919  cbvmpt  3941  axsep2  3966  bnd2  4016  opeqsn  4090  reusv3  4297  tfisi  4417  opeliunxp  4508  eliunxp  4590  relop  4601  eldm2g  4647  reldm0  4669  relrn0  4710  xpmlem  4867  elxp5  4934  cnvpom  4988  cbviota  5000  iota1  5009  sniota  5022  fncnv  5095  fnres  5145  brprcneu  5313  fnopfvb  5361  fvelrnb  5367  fvelimab  5375  fvopab3g  5392  eqfnfv3  5415  eqfnfv2f  5417  fvreseq  5419  fnreseql  5425  rexsupp  5439  respreima  5443  rexrn  5452  ralrn  5453  f1ompt  5466  fsn  5485  fconstfvm  5531  fconst3m  5532  fconst4m  5533  foima2  5546  rexima  5550  ralima  5551  dff13  5563  foeqcnvco  5585  fliftfun  5591  isocnv  5606  isoini  5613  f1oiso  5621  cbvriota  5634  eusvobj2  5654  oprabid  5697  eloprabga  5751  resoprab  5757  eqfnov  5767  eqfnov2  5768  ov6g  5798  funimassov  5810  ovelimab  5811  caovord2  5833  releldm2  5971  dfoprab4  5978  xporderlem  6012  poxp  6013  f1od2  6016  mpt2xopovel  6022  brtpos2  6032  brtpos0  6033  rntpos  6038  dftpos3  6043  tpostpos  6045  tpossym  6057  tposoprab  6061  tfrcllemres  6143  frecabcl  6180  frecsuclem  6187  erth2  6353  qliftfun  6390  erovlem  6400  ecopovsym  6404  ecopovsymg  6407  th3qlem1  6410  mapdm0  6436  elpmg  6437  elpm2g  6438  map0e  6459  dom2lem  6545  mapsnen  6584  xpdom2  6603  xpf1o  6616  mapen  6618  ssfilem  6647  diffitest  6659  ac6sfi  6670  isoti  6758  cnvti  6770  ltexpi  6959  ordpipqqs  6996  ltexnqq  7030  enq0enq  7053  enq0sym  7054  enq0tr  7056  nqnq0pi  7060  genipv  7131  genprndl  7143  genprndu  7144  genpdisj  7145  genpassl  7146  genpassu  7147  addcomprg  7200  mulcomprg  7202  ltnqpr  7215  ltnqpri  7216  ltexprlemm  7222  ltexprlemdisj  7228  ltsrprg  7356  mulgt0sr  7386  elreal2  7431  ltresr  7439  ltresr2  7440  axprecex  7478  axpre-ltadd  7484  axpre-mulgt0  7485  axpre-mulext  7486  subcan2  7770  negcon1  7797  negcon2  7798  lt0neg1  8009  lt0neg2  8010  le0neg1  8011  le0neg2  8012  reapirr  8117  reapmul1  8135  reapneg  8137  remulext1  8139  apti  8162  negap0  8169  divmulap2  8206  reclt1  8420  recgt1  8421  suprleubex  8478  addltmul  8715  elznn0  8828  zapne  8884  zltlen  8888  nn0lt10b  8890  nn0lt2  8891  eluz1  9086  raluz  9129  rexuz  9131  qltlen  9188  cnref1o  9196  rpnegap  9229  ltxr  9309  xlt0neg1  9363  xlt0neg2  9364  xle0neg1  9365  xle0neg2  9366  elixx1  9378  elixx3g  9382  elioo2  9402  icc0r  9407  elicc4  9421  elioopnf  9448  elioomnf  9449  iooneg  9468  iccneg  9469  iccshftr  9474  iccshftl  9476  iccdil  9478  icccntr  9480  iccf1o  9484  elfz1  9492  0fz1  9522  fzpr  9554  fzdifsuc  9558  uzsplit  9569  elfzm1b  9575  elfzp12  9576  fznn0  9590  exfzdc  9714  flqeqceilz  9788  zmodid2  9822  expap0  10048  bernneq  10137  hasheqf1o  10256  hashfacen  10304  sqrtmsq2i  10631  maxclpr  10718  minmax  10724  clim0  10736  climrecvg1n  10800  isummo  10836  fsumsplit  10864  mertenslem2  10993  dvdsval2  11140  odd2np1lem  11213  even2n  11215  divalgb  11266  divalgmod  11268  zsupcllemstep  11282  gcddvds  11296  bezoutlemmain  11328  isprm3  11441  prmind2  11443  dvdsprime  11445  coprm  11464  prmdvdsexp  11468  sqrt2irr  11482  sqpweven  11494  2sqpwodd  11495  elrest  11722  istopon  11775  isbasis2g  11806  isbasis3g  11807  tgss2  11842  bastop1  11846  iscld  11866  ntreq0  11895  elcncf  11933
  Copyright terms: Public domain W3C validator