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  5208  dmfco  5776  omp1eomlem  7440  ltanqg  7773  genpassl  7897  genpassu  7898  ltexprlemloc  7980  caucvgprlemcanl  8017  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemaddq  8081  apneg  8947  lemuldiv  9219  msq11  9240  negiso  9293  avglt2  9556  xleaddadd  10306  iooshf  10371  qtri3or  10692  sq11ap  11166  hashen  11245  fihashdom  11265  cjap  11694  sqrt11ap  11826  mingeb  12033  xrnegiso  12053  clim2c  12075  climabs0  12098  absefib  12563  efieq1re  12564  nndivides  12589  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  halfleoddlt  12686  pc2dvds  13138  pcmpt  13151  issubm  13838  cnntr  15451  cndis  15467  cnpdis  15468  lmres  15474  txhmeo  15545  blininf  15650  cncfmet  15818  bposlem1  16311