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  2790  frecsuclem  6473  indpi  7428  cauappcvgprlemladdru  7742  prsrlt  7873  lesub2  8503  ltsub2  8505  rec11ap  8756  avglt1  9249  rpnegap  9780  modqmuladdnn0  10479  expap0  10680  2shfti  11015  mulreap  11048  minmax  11414  lemininf  11418  xrminmax  11449  xrlemininf  11455  modremain  12113  nnwosdc  12233  nn0seqcvgd  12236  divgcdcoprm0  12296  ismgmid  13081  grpsubeq0  13290  grpsubadd  13292  eqg0el  13437  isunitd  13740  lsslss  14015  isridlrng  14116  zndvds  14283  znleval  14287  isxmet2d  14692  xblss2  14749  neibl  14835  ellimc3apf  15004  logbgt0b  15310  lgsne0  15387  lgsabs1  15388  lgsquadlem1  15426  m1lgs  15434  iswomninnlem  15806