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  8939  lemuldiv  9211  msq11  9232  negiso  9285  avglt2  9545  xleaddadd  10289  iooshf  10354  qtri3or  10675  sq11ap  11145  hashen  11223  fihashdom  11243  cjap  11672  sqrt11ap  11804  mingeb  12008  xrnegiso  12028  clim2c  12050  climabs0  12073  absefib  12538  efieq1re  12539  nndivides  12564  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  halfleoddlt  12661  pc2dvds  13109  pcmpt  13122  issubm  13779  cnntr  15326  cndis  15342  cnpdis  15343  lmres  15349  txhmeo  15420  blininf  15525  cncfmet  15693