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  5088  dmfco  5632  omp1eomlem  7169  ltanqg  7486  genpassl  7610  genpassu  7611  ltexprlemloc  7693  caucvgprlemcanl  7730  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  caucvgprprlemaddq  7794  apneg  8657  lemuldiv  8927  msq11  8948  negiso  9001  avglt2  9250  xleaddadd  9981  iooshf  10046  qtri3or  10349  sq11ap  10818  hashen  10895  fihashdom  10914  cjap  11090  sqrt11ap  11222  mingeb  11426  xrnegiso  11446  clim2c  11468  climabs0  11491  absefib  11955  efieq1re  11956  nndivides  11981  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  halfleoddlt  12078  pc2dvds  12526  pcmpt  12539  issubm  13176  cnntr  14569  cndis  14585  cnpdis  14586  lmres  14592  txhmeo  14663  blininf  14768  cncfmet  14936