Theorem 3bitr4rd 221

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 191	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 191	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:  inimasn  5145  dmfco  5701  omp1eomlem  7257  ltanqg  7583  genpassl  7707  genpassu  7708  ltexprlemloc  7790  caucvgprlemcanl  7827  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgprprlemaddq  7891  apneg  8754  lemuldiv  9024  msq11  9045  negiso  9098  avglt2  9347  xleaddadd  10079  iooshf  10144  qtri3or  10455  sq11ap  10924  hashen  11001  fihashdom  11020  cjap  11412  sqrt11ap  11544  mingeb  11748  xrnegiso  11768  clim2c  11790  climabs0  11813  absefib  12277  efieq1re  12278  nndivides  12303  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  halfleoddlt  12400  pc2dvds  12848  pcmpt  12861  issubm  13500  cnntr  14893  cndis  14909  cnpdis  14910  lmres  14916  txhmeo  14987  blininf  15092  cncfmet  15260