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  5180  dmfco  5745  omp1eomlem  7385  ltanqg  7715  genpassl  7839  genpassu  7840  ltexprlemloc  7922  caucvgprlemcanl  7959  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgprprlemaddq  8023  apneg  8885  lemuldiv  9155  msq11  9176  negiso  9229  avglt2  9478  xleaddadd  10220  iooshf  10285  qtri3or  10600  sq11ap  11069  hashen  11147  fihashdom  11167  cjap  11591  sqrt11ap  11723  mingeb  11927  xrnegiso  11947  clim2c  11969  climabs0  11992  absefib  12457  efieq1re  12458  nndivides  12483  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  halfleoddlt  12580  pc2dvds  13028  pcmpt  13041  issubm  13685  cnntr  15090  cndis  15106  cnpdis  15107  lmres  15113  txhmeo  15184  blininf  15289  cncfmet  15457