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  7150  ordpipqqs  7187  ltexnqq  7221  enq0enq  7244  enq0sym  7245  enq0tr  7247  nqnq0pi  7251  genipv  7322  genprndl  7334  genprndu  7335  genpdisj  7336  genpassl  7337  genpassu  7338  addcomprg  7391  mulcomprg  7393  ltnqpr  7406  ltnqpri  7407  ltexprlemm  7413  ltexprlemdisj  7419  suplocexprlemmu  7531  suplocexprlemdisj  7533  ltsrprg  7560  mulgt0sr  7591  elreal2  7643  ltresr  7652  ltresr2  7653  axprecex  7693  axpre-ltadd  7699  axpre-mulgt0  7700  axpre-mulext  7701  axpre-suploclemres  7714  subcan2  7992  negcon1  8019  negcon2  8020  lt0neg1  8235  lt0neg2  8236  le0neg1  8237  le0neg2  8238  reapirr  8344  reapmul1  8362  reapneg  8364  remulext1  8366  apti  8389  negap0  8397  divmulap2  8441  reclt1  8659  recgt1  8660  suprleubex  8717  addltmul  8961  elznn0  9074  zapne  9130  zltlen  9134  nn0lt10b  9136  nn0lt2  9137  eluz1  9335  raluz  9378  rexuz  9380  qltlen  9437  cnref1o  9445  rpnegap  9479  ltxr  9567  xlt0neg1  9626  xlt0neg2  9627  xle0neg1  9628  xle0neg2  9629  elixx1  9685  elixx3g  9689  elioo2  9709  icc0r  9714  elicc4  9728  elioopnf  9755  elioomnf  9756  iooneg  9776  iccneg  9777  iccshftr  9782  iccshftl  9784  iccdil  9786  icccntr  9788  iccf1o  9792  elfz1  9800  0fz1  9830  fzpr  9862  fzdifsuc  9866  uzsplit  9877  elfzm1b  9883  elfzp12  9884  fznn0  9898  exfzdc  10022  flqeqceilz  10096  zmodid2  10130  expap0  10328  bernneq  10417  hasheqf1o  10536  hashfacen  10584  sqrtmsq2i  10912  maxclpr  10999  minmax  11006  xrmaxlesup  11033  xrnegiso  11036  xrnegcon1d  11038  xrminmax  11039  clim0  11059  climrecvg1n  11122  summodc  11157  fsumsplit  11181  mertenslem2  11310  prodmodc  11352  dvdsval2  11501  odd2np1lem  11574  even2n  11576  divalgb  11627  divalgmod  11629  zsupcllemstep  11643  gcddvds  11657  bezoutlemmain  11691  isprm3  11804  prmind2  11806  dvdsprime  11808  coprm  11827  prmdvdsexp  11831  sqrt2irr  11845  sqpweven  11858  2sqpwodd  11859  elrest  12132  istopon  12185  isbasis2g  12217  isbasis3g  12218  tgss2  12253  bastop1  12257  iscld  12277  ntreq0  12306  restsn  12354  restopn2  12357  lmbr  12387  cnptoprest2  12414  txbas  12432  eltx  12433  txlm  12453  ishmeo  12478  hmeoimaf1o  12488  ispsmet  12497  ismet  12518  isxmet  12519  ismet2  12528  metn0  12552  elblps  12564  elbl  12565  bdbl  12677  qtopbasss  12695  elcncf  12734  ellimc3apf  12803  sincosq1sgn  12912  sincosq2sgn  12913  subctctexmid  13201