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  11159  hashen  11238  fihashdom  11258  cjap  11687  sqrt11ap  11819  mingeb  12026  xrnegiso  12046  clim2c  12068  climabs0  12091  absefib  12556  efieq1re  12557  nndivides  12582  oddnn02np1  12665  oddge22np1  12666  evennn02n  12667  evennn2n  12668  halfleoddlt  12679  pc2dvds  13131  pcmpt  13144  issubm  13830  cnntr  15378  cndis  15394  cnpdis  15395  lmres  15401  txhmeo  15472  blininf  15577  cncfmet  15745  bposlem1  16233