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  7434  ltanqg  7767  genpassl  7891  genpassu  7892  ltexprlemloc  7974  caucvgprlemcanl  8011  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemaddq  8075  apneg  8941  lemuldiv  9213  msq11  9234  negiso  9287  avglt2  9549  xleaddadd  10299  iooshf  10364  qtri3or  10685  sq11ap  11158  hashen  11237  fihashdom  11257  cjap  11686  sqrt11ap  11818  mingeb  12024  xrnegiso  12044  clim2c  12066  climabs0  12089  absefib  12554  efieq1re  12555  nndivides  12580  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  halfleoddlt  12677  pc2dvds  13129  pcmpt  13142  issubm  13828  cnntr  15375  cndis  15391  cnpdis  15392  lmres  15398  txhmeo  15469  blininf  15574  cncfmet  15742  bposlem1  16209