Theorem 3bitrd 214

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))
3bitrd.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitrd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	1, 2	bitrd 188	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sbceqal  3053  sbcnel12g  3109  elxp4  5167  elxp5  5168  f1eq123d  5508  foeq123d  5509  f1oeq123d  5510  fnmptfvd  5678  ofrfval  6157  eloprabi  6272  fnmpoovd  6291  smoeq  6366  ecidg  6676  ixpsnval  6778  enqbreq2  7452  ltanqg  7495  caucvgprprlemexb  7802  caucvgsrlemgt1  7890  caucvgsrlemoffres  7895  ltrennb  7949  apneg  8666  mulext1  8667  apdivmuld  8868  ltdiv23  8947  lediv23  8948  halfpos  9250  addltmul  9256  div4p1lem1div2  9273  ztri3or  9397  supminfex  9700  iccf1o  10108  fzshftral  10212  fzoshftral  10348  infssuzex  10357  2tnp1ge0ge0  10425  fihashen1  10925  seq3coll  10968  cjap  11136  negfi  11458  tanaddaplem  11968  dvdssub  12068  addmodlteqALT  12089  dvdsmod  12092  oddp1even  12106  nn0o1gt2  12135  nn0oddm1d2  12139  bitscmp  12188  cncongr1  12344  cncongr2  12345  4sqlem11  12643  4sqlem17  12649  intopsn  13117  sgrp1  13161  sgrppropd  13163  issubg  13427  nmzsubg  13464  conjnmzb  13534  srg1zr  13667  ring1  13739  issubrg  13901  znf1o  14331  znleval  14333  znunit  14339  elmopn  14836  metss  14884  comet  14889  xmetxp  14897  limcmpted  15053  cnlimc  15062  lgsneg  15419  lgsne0  15433  lgsprme0  15437  lgsquadlem1  15472  lgsquadlem2  15473  2lgs  15499  2lgsoddprm  15508