Theorem 3bitr4rd 220

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4rd	⊢ (𝜑 → (𝜏 ↔ 𝜃))

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr4d 190	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 190	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:  inimasn  4951  dmfco  5482  omp1eomlem  6972  ltanqg  7201  genpassl  7325  genpassu  7326  ltexprlemloc  7408  caucvgprlemcanl  7445  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  caucvgprprlemaddq  7509  apneg  8366  lemuldiv  8632  msq11  8653  negiso  8706  avglt2  8952  xleaddadd  9663  iooshf  9728  qtri3or  10013  sq11ap  10451  hashen  10523  fihashdom  10542  cjap  10671  sqrt11ap  10803  xrnegiso  11024  clim2c  11046  climabs0  11069  absefib  11466  efieq1re  11467  nndivides  11489  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  halfleoddlt  11580  cnntr  12383  cndis  12399  cnpdis  12400  lmres  12406  txhmeo  12477  blininf  12582  cncfmet  12737