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 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  inimasn  5205  dmfco  5773  omp1eomlem  7435  ltanqg  7768  genpassl  7892  genpassu  7893  ltexprlemloc  7975  caucvgprlemcanl  8012  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemaddq  8076  apneg  8942  lemuldiv  9214  msq11  9235  negiso  9288  avglt2  9550  xleaddadd  10300  iooshf  10365  qtri3or  10686  sq11ap  11160  hashen  11239  fihashdom  11259  cjap  11688  sqrt11ap  11820  mingeb  12027  xrnegiso  12047  clim2c  12069  climabs0  12092  absefib  12557  efieq1re  12558  nndivides  12583  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  halfleoddlt  12680  pc2dvds  13132  pcmpt  13145  issubm  13832  cnntr  15417  cndis  15433  cnpdis  15434  lmres  15440  txhmeo  15511  blininf  15616  cncfmet  15784  bposlem1  16272