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  3045  sbcnel12g  3101  elxp4  5157  elxp5  5158  f1eq123d  5496  foeq123d  5497  f1oeq123d  5498  fnmptfvd  5666  ofrfval  6144  eloprabi  6254  fnmpoovd  6273  smoeq  6348  ecidg  6658  ixpsnval  6760  enqbreq2  7424  ltanqg  7467  caucvgprprlemexb  7774  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  ltrennb  7921  apneg  8638  mulext1  8639  apdivmuld  8840  ltdiv23  8919  lediv23  8920  halfpos  9222  addltmul  9228  div4p1lem1div2  9245  ztri3or  9369  supminfex  9671  iccf1o  10079  fzshftral  10183  fzoshftral  10314  infssuzex  10323  2tnp1ge0ge0  10391  fihashen1  10891  seq3coll  10934  cjap  11071  negfi  11393  tanaddaplem  11903  dvdssub  12003  addmodlteqALT  12024  dvdsmod  12027  oddp1even  12041  nn0o1gt2  12070  nn0oddm1d2  12074  cncongr1  12271  cncongr2  12272  4sqlem11  12570  4sqlem17  12576  intopsn  13010  sgrp1  13054  sgrppropd  13056  issubg  13303  nmzsubg  13340  conjnmzb  13410  srg1zr  13543  ring1  13615  issubrg  13777  znf1o  14207  znleval  14209  znunit  14215  elmopn  14682  metss  14730  comet  14735  xmetxp  14743  limcmpted  14899  cnlimc  14908  lgsneg  15265  lgsne0  15279  lgsprme0  15283  lgsquadlem1  15318  lgsquadlem2  15319  2lgs  15345  2lgsoddprm  15354