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  5152  dmfco  5710  omp1eomlem  7284  ltanqg  7610  genpassl  7734  genpassu  7735  ltexprlemloc  7817  caucvgprlemcanl  7854  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgprprlemaddq  7918  apneg  8781  lemuldiv  9051  msq11  9072  negiso  9125  avglt2  9374  xleaddadd  10112  iooshf  10177  qtri3or  10490  sq11ap  10959  hashen  11036  fihashdom  11056  cjap  11457  sqrt11ap  11589  mingeb  11793  xrnegiso  11813  clim2c  11835  climabs0  11858  absefib  12322  efieq1re  12323  nndivides  12348  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  halfleoddlt  12445  pc2dvds  12893  pcmpt  12906  issubm  13545  cnntr  14939  cndis  14955  cnpdis  14956  lmres  14962  txhmeo  15033  blininf  15138  cncfmet  15306