Theorem 3bitr2d 216

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 191	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.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:  ceqsralt  2779  frecsuclem  6432  indpi  7372  cauappcvgprlemladdru  7686  prsrlt  7817  lesub2  8445  ltsub2  8447  rec11ap  8698  avglt1  9188  rpnegap  9718  modqmuladdnn0  10401  expap0  10584  2shfti  10875  mulreap  10908  minmax  11273  lemininf  11277  xrminmax  11308  xrlemininf  11314  modremain  11969  nnwosdc  12075  nn0seqcvgd  12076  divgcdcoprm0  12136  ismgmid  12856  grpsubeq0  13045  grpsubadd  13047  eqg0el  13185  isunitd  13473  lsslss  13714  isridlrng  13815  isxmet2d  14325  xblss2  14382  neibl  14468  ellimc3apf  14606  logbgt0b  14861  lgsne0  14917  lgsabs1  14918  m1lgs  14930  iswomninnlem  15276