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  2828  frecsuclem  6567  indpi  7555  cauappcvgprlemladdru  7869  prsrlt  8000  lesub2  8630  ltsub2  8632  rec11ap  8883  avglt1  9376  rpnegap  9914  modqmuladdnn0  10623  expap0  10824  swrdspsleq  11241  2shfti  11385  mulreap  11418  minmax  11784  lemininf  11788  xrminmax  11819  xrlemininf  11825  modremain  12483  nnwosdc  12603  nn0seqcvgd  12606  divgcdcoprm0  12666  ismgmid  13453  grpsubeq0  13662  grpsubadd  13664  eqg0el  13809  isunitd  14113  lsslss  14388  isridlrng  14489  zndvds  14656  znleval  14660  isxmet2d  15065  xblss2  15122  neibl  15208  ellimc3apf  15377  logbgt0b  15683  lgsne0  15760  lgsabs1  15761  lgsquadlem1  15799  m1lgs  15807  iswomninnlem  16603