Theorem 3bitr2d 215

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 190	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	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:  ceqsralt  2757  frecsuclem  6385  indpi  7304  cauappcvgprlemladdru  7618  prsrlt  7749  lesub2  8376  ltsub2  8378  rec11ap  8627  avglt1  9116  rpnegap  9643  modqmuladdnn0  10324  expap0  10506  2shfti  10795  mulreap  10828  minmax  11193  lemininf  11197  xrminmax  11228  xrlemininf  11234  modremain  11888  nn0seqcvgd  11995  divgcdcoprm0  12055  ismgmid  12631  isxmet2d  13142  xblss2  13199  neibl  13285  ellimc3apf  13423  logbgt0b  13678  lgsne0  13733  lgsabs1  13734  iswomninnlem  14081