Theorem syl6bb 195

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6bb.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6bb.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
syl6bb	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6bb.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 187	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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  873  pm5.75  946  xordidc  1377  19.17  1535  alexdc  1598  nf4dc  1648  abeq2d  2252  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvrab  2684  ceqsralt  2713  ralab2  2848  rexab2  2850  euxfr2dc  2869  reu7  2879  reu8  2880  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  ralss  3163  rexss  3164  prssg  3677  2ralunsn  3725  eluniab  3748  elintab  3782  dfiun2g  3845  dfiin2g  3846  cbvopab1  4001  cbvmpt  4023  axsep2  4047  bnd2  4097  opeqsn  4174  reusv3  4381  tfisi  4501  opeliunxp  4594  eliunxp  4678  relop  4689  eldm2g  4735  reldm0  4757  relrn0  4801  xpmlem  4959  elxp5  5027  cnvpom  5081  cbviota  5093  iota1  5102  sniota  5115  fncnv  5189  fnres  5239  brprcneu  5414  fnopfvb  5463  fvelrnb  5469  fvelimab  5477  fvopab3g  5494  eqfnfv3  5520  eqfnfv2f  5522  fvreseq  5524  fnreseql  5530  rexsupp  5544  respreima  5548  rexrn  5557  ralrn  5558  f1ompt  5571  fsn  5592  fconstfvm  5638  fconst3m  5639  fconst4m  5640  foima2  5653  rexima  5656  ralima  5657  dff13  5669  foeqcnvco  5691  fliftfun  5697  isocnv  5712  isoini  5719  f1oiso  5727  cbvriota  5740  eusvobj2  5760  oprabid  5803  eloprabga  5858  resoprab  5867  eqfnov  5877  eqfnov2  5878  ov6g  5908  funimassov  5920  ovelimab  5921  caovord2  5943  releldm2  6083  dfoprab4  6090  xporderlem  6128  poxp  6129  f1od2  6132  mpoxopovel  6138  brtpos2  6148  brtpos0  6149  rntpos  6154  dftpos3  6159  tpostpos  6161  tpossym  6173  tposoprab  6177  tfrcllemres  6259  frecabcl  6296  frecsuclem  6303  erth2  6474  qliftfun  6511  erovlem  6521  ecopovsym  6525  ecopovsymg  6528  th3qlem1  6531  mapdm0  6557  elpmg  6558  elpm2g  6559  map0e  6580  dom2lem  6666  mapsnen  6705  xpdom2  6725  xpf1o  6738  mapen  6740  ssfilem  6769  diffitest  6781  ac6sfi  6792  isoti  6894  cnvti  6906  omp1eomlem  6979  ismkvnex  7029  ltexpi  7145  ordpipqqs  7182  ltexnqq  7216  enq0enq  7239  enq0sym  7240  enq0tr  7242  nqnq0pi  7246  genipv  7317  genprndl  7329  genprndu  7330  genpdisj  7331  genpassl  7332  genpassu  7333  addcomprg  7386  mulcomprg  7388  ltnqpr  7401  ltnqpri  7402  ltexprlemm  7408  ltexprlemdisj  7414  suplocexprlemmu  7526  suplocexprlemdisj  7528  ltsrprg  7555  mulgt0sr  7586  elreal2  7638  ltresr  7647  ltresr2  7648  axprecex  7688  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  axpre-suploclemres  7709  subcan2  7987  negcon1  8014  negcon2  8015  lt0neg1  8230  lt0neg2  8231  le0neg1  8232  le0neg2  8233  reapirr  8339  reapmul1  8357  reapneg  8359  remulext1  8361  apti  8384  negap0  8392  divmulap2  8436  reclt1  8654  recgt1  8655  suprleubex  8712  addltmul  8956  elznn0  9069  zapne  9125  zltlen  9129  nn0lt10b  9131  nn0lt2  9132  eluz1  9330  raluz  9373  rexuz  9375  qltlen  9432  cnref1o  9440  rpnegap  9474  ltxr  9562  xlt0neg1  9621  xlt0neg2  9622  xle0neg1  9623  xle0neg2  9624  elixx1  9680  elixx3g  9684  elioo2  9704  icc0r  9709  elicc4  9723  elioopnf  9750  elioomnf  9751  iooneg  9771  iccneg  9772  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  iccf1o  9787  elfz1  9795  0fz1  9825  fzpr  9857  fzdifsuc  9861  uzsplit  9872  elfzm1b  9878  elfzp12  9879  fznn0  9893  exfzdc  10017  flqeqceilz  10091  zmodid2  10125  expap0  10323  bernneq  10412  hasheqf1o  10531  hashfacen  10579  sqrtmsq2i  10907  maxclpr  10994  minmax  11001  xrmaxlesup  11028  xrnegiso  11031  xrnegcon1d  11033  xrminmax  11034  clim0  11054  climrecvg1n  11117  summodc  11152  fsumsplit  11176  mertenslem2  11305  prodmodc  11347  dvdsval2  11496  odd2np1lem  11569  even2n  11571  divalgb  11622  divalgmod  11624  zsupcllemstep  11638  gcddvds  11652  bezoutlemmain  11686  isprm3  11799  prmind2  11801  dvdsprime  11803  coprm  11822  prmdvdsexp  11826  sqrt2irr  11840  sqpweven  11853  2sqpwodd  11854  elrest  12127  istopon  12180  isbasis2g  12212  isbasis3g  12213  tgss2  12248  bastop1  12252  iscld  12272  ntreq0  12301  restsn  12349  restopn2  12352  lmbr  12382  cnptoprest2  12409  txbas  12427  eltx  12428  txlm  12448  ishmeo  12473  hmeoimaf1o  12483  ispsmet  12492  ismet  12513  isxmet  12514  ismet2  12523  metn0  12547  elblps  12559  elbl  12560  bdbl  12672  qtopbasss  12690  elcncf  12729  ellimc3apf  12798  sincosq1sgn  12907  sincosq2sgn  12908  subctctexmid  13196