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-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:  syl6rbb  196  syl6bbr  197  3bitr3g  221  bibi2i  226  ibibr  245  biancomd  269  imanst  858  pm5.75  931  xordidc  1362  19.17  1520  alexdc  1583  nf4dc  1633  abeq2d  2230  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvrab  2658  ceqsralt  2687  ralab2  2821  rexab2  2823  euxfr2dc  2842  reu7  2852  reu8  2853  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  ralss  3133  rexss  3134  prssg  3647  2ralunsn  3695  eluniab  3718  elintab  3752  dfiun2g  3815  dfiin2g  3816  cbvopab1  3971  cbvmpt  3993  axsep2  4017  bnd2  4067  opeqsn  4144  reusv3  4351  tfisi  4471  opeliunxp  4564  eliunxp  4648  relop  4659  eldm2g  4705  reldm0  4727  relrn0  4771  xpmlem  4929  elxp5  4997  cnvpom  5051  cbviota  5063  iota1  5072  sniota  5085  fncnv  5159  fnres  5209  brprcneu  5382  fnopfvb  5431  fvelrnb  5437  fvelimab  5445  fvopab3g  5462  eqfnfv3  5488  eqfnfv2f  5490  fvreseq  5492  fnreseql  5498  rexsupp  5512  respreima  5516  rexrn  5525  ralrn  5526  f1ompt  5539  fsn  5560  fconstfvm  5606  fconst3m  5607  fconst4m  5608  foima2  5621  rexima  5624  ralima  5625  dff13  5637  foeqcnvco  5659  fliftfun  5665  isocnv  5680  isoini  5687  f1oiso  5695  cbvriota  5708  eusvobj2  5728  oprabid  5771  eloprabga  5826  resoprab  5835  eqfnov  5845  eqfnov2  5846  ov6g  5876  funimassov  5888  ovelimab  5889  caovord2  5911  releldm2  6051  dfoprab4  6058  xporderlem  6096  poxp  6097  f1od2  6100  mpoxopovel  6106  brtpos2  6116  brtpos0  6117  rntpos  6122  dftpos3  6127  tpostpos  6129  tpossym  6141  tposoprab  6145  tfrcllemres  6227  frecabcl  6264  frecsuclem  6271  erth2  6442  qliftfun  6479  erovlem  6489  ecopovsym  6493  ecopovsymg  6496  th3qlem1  6499  mapdm0  6525  elpmg  6526  elpm2g  6527  map0e  6548  dom2lem  6634  mapsnen  6673  xpdom2  6693  xpf1o  6706  mapen  6708  ssfilem  6737  diffitest  6749  ac6sfi  6760  isoti  6862  cnvti  6874  omp1eomlem  6947  ismkvnex  6997  ltexpi  7113  ordpipqqs  7150  ltexnqq  7184  enq0enq  7207  enq0sym  7208  enq0tr  7210  nqnq0pi  7214  genipv  7285  genprndl  7297  genprndu  7298  genpdisj  7299  genpassl  7300  genpassu  7301  addcomprg  7354  mulcomprg  7356  ltnqpr  7369  ltnqpri  7370  ltexprlemm  7376  ltexprlemdisj  7382  suplocexprlemmu  7494  suplocexprlemdisj  7496  ltsrprg  7523  mulgt0sr  7554  elreal2  7606  ltresr  7615  ltresr2  7616  axprecex  7656  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  axpre-suploclemres  7677  subcan2  7955  negcon1  7982  negcon2  7983  lt0neg1  8198  lt0neg2  8199  le0neg1  8200  le0neg2  8201  reapirr  8306  reapmul1  8324  reapneg  8326  remulext1  8328  apti  8351  negap0  8359  divmulap2  8403  reclt1  8618  recgt1  8619  suprleubex  8676  addltmul  8914  elznn0  9027  zapne  9083  zltlen  9087  nn0lt10b  9089  nn0lt2  9090  eluz1  9286  raluz  9329  rexuz  9331  qltlen  9388  cnref1o  9396  rpnegap  9429  ltxr  9517  xlt0neg1  9576  xlt0neg2  9577  xle0neg1  9578  xle0neg2  9579  elixx1  9635  elixx3g  9639  elioo2  9659  icc0r  9664  elicc4  9678  elioopnf  9705  elioomnf  9706  iooneg  9726  iccneg  9727  iccshftr  9732  iccshftl  9734  iccdil  9736  icccntr  9738  iccf1o  9742  elfz1  9750  0fz1  9780  fzpr  9812  fzdifsuc  9816  uzsplit  9827  elfzm1b  9833  elfzp12  9834  fznn0  9848  exfzdc  9972  flqeqceilz  10046  zmodid2  10080  expap0  10278  bernneq  10367  hasheqf1o  10486  hashfacen  10534  sqrtmsq2i  10862  maxclpr  10949  minmax  10956  xrmaxlesup  10983  xrnegiso  10986  xrnegcon1d  10988  xrminmax  10989  clim0  11009  climrecvg1n  11072  summodc  11107  fsumsplit  11131  mertenslem2  11260  dvdsval2  11408  odd2np1lem  11481  even2n  11483  divalgb  11534  divalgmod  11536  zsupcllemstep  11550  gcddvds  11564  bezoutlemmain  11598  isprm3  11711  prmind2  11713  dvdsprime  11715  coprm  11734  prmdvdsexp  11738  sqrt2irr  11752  sqpweven  11764  2sqpwodd  11765  elrest  12038  istopon  12091  isbasis2g  12123  isbasis3g  12124  tgss2  12159  bastop1  12163  iscld  12183  ntreq0  12212  restsn  12260  restopn2  12263  lmbr  12293  cnptoprest2  12320  txbas  12338  eltx  12339  txlm  12359  ishmeo  12384  hmeoimaf1o  12394  ispsmet  12403  ismet  12424  isxmet  12425  ismet2  12434  metn0  12458  elblps  12470  elbl  12471  bdbl  12583  qtopbasss  12601  elcncf  12640  ellimc3apf  12709  sincosq1sgn  12818  sincosq2sgn  12819  subctctexmid  13092
  Copyright terms: Public domain W3C validator