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  7426  cauappcvgprlemladdru  7740  prsrlt  7871  lesub2  8501  ltsub2  8503  rec11ap  8754  avglt1  9247  rpnegap  9778  modqmuladdnn0  10477  expap0  10678  2shfti  11013  mulreap  11046  minmax  11412  lemininf  11416  xrminmax  11447  xrlemininf  11453  modremain  12111  nnwosdc  12231  nn0seqcvgd  12234  divgcdcoprm0  12294  ismgmid  13079  grpsubeq0  13288  grpsubadd  13290  eqg0el  13435  isunitd  13738  lsslss  14013  isridlrng  14114  zndvds  14281  znleval  14285  isxmet2d  14668  xblss2  14725  neibl  14811  ellimc3apf  14980  logbgt0b  15286  lgsne0  15363  lgsabs1  15364  lgsquadlem1  15402  m1lgs  15410  iswomninnlem  15780