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  5161  dmfco  5723  omp1eomlem  7336  ltanqg  7663  genpassl  7787  genpassu  7788  ltexprlemloc  7870  caucvgprlemcanl  7907  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemaddq  7971  apneg  8833  lemuldiv  9103  msq11  9124  negiso  9177  avglt2  9426  xleaddadd  10166  iooshf  10231  qtri3or  10546  sq11ap  11015  hashen  11092  fihashdom  11112  cjap  11529  sqrt11ap  11661  mingeb  11865  xrnegiso  11885  clim2c  11907  climabs0  11930  absefib  12395  efieq1re  12396  nndivides  12421  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  halfleoddlt  12518  pc2dvds  12966  pcmpt  12979  issubm  13618  cnntr  15019  cndis  15035  cnpdis  15036  lmres  15042  txhmeo  15113  blininf  15218  cncfmet  15386