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  2827  frecsuclem  6563  indpi  7545  cauappcvgprlemladdru  7859  prsrlt  7990  lesub2  8620  ltsub2  8622  rec11ap  8873  avglt1  9366  rpnegap  9899  modqmuladdnn0  10607  expap0  10808  swrdspsleq  11220  2shfti  11363  mulreap  11396  minmax  11762  lemininf  11766  xrminmax  11797  xrlemininf  11803  modremain  12461  nnwosdc  12581  nn0seqcvgd  12584  divgcdcoprm0  12644  ismgmid  13431  grpsubeq0  13640  grpsubadd  13642  eqg0el  13787  isunitd  14091  lsslss  14366  isridlrng  14467  zndvds  14634  znleval  14638  isxmet2d  15043  xblss2  15100  neibl  15186  ellimc3apf  15355  logbgt0b  15661  lgsne0  15738  lgsabs1  15739  lgsquadlem1  15777  m1lgs  15785  iswomninnlem  16531