Theorem 3bitr4rd 220

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 190	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 190	1 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  inimasn  4964  dmfco  5497  omp1eomlem  6987  ltanqg  7232  genpassl  7356  genpassu  7357  ltexprlemloc  7439  caucvgprlemcanl  7476  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  caucvgprprlemaddq  7540  apneg  8397  lemuldiv  8663  msq11  8684  negiso  8737  avglt2  8983  xleaddadd  9700  iooshf  9765  qtri3or  10051  sq11ap  10489  hashen  10562  fihashdom  10581  cjap  10710  sqrt11ap  10842  xrnegiso  11063  clim2c  11085  climabs0  11108  absefib  11513  efieq1re  11514  nndivides  11536  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  halfleoddlt  11627  cnntr  12433  cndis  12449  cnpdis  12450  lmres  12456  txhmeo  12527  blininf  12632  cncfmet  12787