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-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  856  pm5.75  929  xordidc  1360  19.17  1518  alexdc  1581  nf4dc  1631  abeq2d  2227  cbvralf  2622  cbvrexf  2623  cbvreu  2626  cbvrab  2655  ceqsralt  2684  ralab2  2817  rexab2  2819  euxfr2dc  2838  reu7  2848  reu8  2849  cbvralcsf  3028  cbvrexcsf  3029  cbvreucsf  3030  cbvrabcsf  3031  ralss  3129  rexss  3130  prssg  3643  2ralunsn  3691  eluniab  3714  elintab  3748  dfiun2g  3811  dfiin2g  3812  cbvopab1  3961  cbvmpt  3983  axsep2  4007  bnd2  4057  opeqsn  4134  reusv3  4341  tfisi  4461  opeliunxp  4554  eliunxp  4638  relop  4649  eldm2g  4695  reldm0  4717  relrn0  4759  xpmlem  4917  elxp5  4985  cnvpom  5039  cbviota  5051  iota1  5060  sniota  5073  fncnv  5147  fnres  5197  brprcneu  5368  fnopfvb  5417  fvelrnb  5423  fvelimab  5431  fvopab3g  5448  eqfnfv3  5474  eqfnfv2f  5476  fvreseq  5478  fnreseql  5484  rexsupp  5498  respreima  5502  rexrn  5511  ralrn  5512  f1ompt  5525  fsn  5546  fconstfvm  5592  fconst3m  5593  fconst4m  5594  foima2  5607  rexima  5610  ralima  5611  dff13  5623  foeqcnvco  5645  fliftfun  5651  isocnv  5666  isoini  5673  f1oiso  5681  cbvriota  5694  eusvobj2  5714  oprabid  5757  eloprabga  5812  resoprab  5821  eqfnov  5831  eqfnov2  5832  ov6g  5862  funimassov  5874  ovelimab  5875  caovord2  5897  releldm2  6037  dfoprab4  6044  xporderlem  6082  poxp  6083  f1od2  6086  mpoxopovel  6092  brtpos2  6102  brtpos0  6103  rntpos  6108  dftpos3  6113  tpostpos  6115  tpossym  6127  tposoprab  6131  tfrcllemres  6213  frecabcl  6250  frecsuclem  6257  erth2  6428  qliftfun  6465  erovlem  6475  ecopovsym  6479  ecopovsymg  6482  th3qlem1  6485  mapdm0  6511  elpmg  6512  elpm2g  6513  map0e  6534  dom2lem  6620  mapsnen  6659  xpdom2  6678  xpf1o  6691  mapen  6693  ssfilem  6722  diffitest  6734  ac6sfi  6745  isoti  6846  cnvti  6858  omp1eomlem  6931  ismkvnex  6979  ltexpi  7093  ordpipqqs  7130  ltexnqq  7164  enq0enq  7187  enq0sym  7188  enq0tr  7190  nqnq0pi  7194  genipv  7265  genprndl  7277  genprndu  7278  genpdisj  7279  genpassl  7280  genpassu  7281  addcomprg  7334  mulcomprg  7336  ltnqpr  7349  ltnqpri  7350  ltexprlemm  7356  ltexprlemdisj  7362  ltsrprg  7490  mulgt0sr  7520  elreal2  7565  ltresr  7574  ltresr2  7575  axprecex  7615  axpre-ltadd  7621  axpre-mulgt0  7622  axpre-mulext  7623  subcan2  7910  negcon1  7937  negcon2  7938  lt0neg1  8149  lt0neg2  8150  le0neg1  8151  le0neg2  8152  reapirr  8257  reapmul1  8275  reapneg  8277  remulext1  8279  apti  8302  negap0  8310  divmulap2  8349  reclt1  8564  recgt1  8565  suprleubex  8622  addltmul  8860  elznn0  8973  zapne  9029  zltlen  9033  nn0lt10b  9035  nn0lt2  9036  eluz1  9232  raluz  9275  rexuz  9277  qltlen  9334  cnref1o  9342  rpnegap  9375  ltxr  9455  xlt0neg1  9514  xlt0neg2  9515  xle0neg1  9516  xle0neg2  9517  elixx1  9573  elixx3g  9577  elioo2  9597  icc0r  9602  elicc4  9616  elioopnf  9643  elioomnf  9644  iooneg  9664  iccneg  9665  iccshftr  9670  iccshftl  9672  iccdil  9674  icccntr  9676  iccf1o  9680  elfz1  9688  0fz1  9718  fzpr  9750  fzdifsuc  9754  uzsplit  9765  elfzm1b  9771  elfzp12  9772  fznn0  9786  exfzdc  9910  flqeqceilz  9984  zmodid2  10018  expap0  10216  bernneq  10305  hasheqf1o  10424  hashfacen  10472  sqrtmsq2i  10799  maxclpr  10886  minmax  10893  xrmaxlesup  10920  xrnegiso  10923  xrnegcon1d  10925  xrminmax  10926  clim0  10946  climrecvg1n  11009  summodc  11044  fsumsplit  11068  mertenslem2  11197  dvdsval2  11344  odd2np1lem  11417  even2n  11419  divalgb  11470  divalgmod  11472  zsupcllemstep  11486  gcddvds  11500  bezoutlemmain  11532  isprm3  11645  prmind2  11647  dvdsprime  11649  coprm  11668  prmdvdsexp  11672  sqrt2irr  11686  sqpweven  11698  2sqpwodd  11699  elrest  11970  istopon  12023  isbasis2g  12055  isbasis3g  12056  tgss2  12091  bastop1  12095  iscld  12115  ntreq0  12144  restsn  12192  restopn2  12195  lmbr  12224  cnptoprest2  12251  txbas  12269  eltx  12270  txlm  12290  ispsmet  12312  ismet  12333  isxmet  12334  ismet2  12343  metn0  12367  elblps  12379  elbl  12380  bdbl  12492  qtopbasss  12510  elcncf  12546  ellimc3apf  12585  subctctexmid  12888