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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  inimasn  4892  dmfco  5421  omp1eomlem  6894  ltanqg  7109  genpassl  7233  genpassu  7234  ltexprlemloc  7316  caucvgprlemcanl  7353  cauappcvgprlemladdrl  7366  caucvgprlemladdrl  7387  caucvgprprlemaddq  7417  apneg  8239  lemuldiv  8497  msq11  8518  negiso  8571  avglt2  8811  xleaddadd  9511  iooshf  9576  qtri3or  9861  sq11ap  10299  hashen  10371  fihashdom  10390  cjap  10519  sqrt11ap  10650  xrnegiso  10870  clim2c  10892  climabs0  10915  absefib  11274  efieq1re  11275  nndivides  11295  oddnn02np1  11372  oddge22np1  11373  evennn02n  11374  evennn2n  11375  halfleoddlt  11386  cnntr  12175  cndis  12191  cnpdis  12192  lmres  12198  blininf  12352  cncfmet  12492