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 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  inimasn  5200  dmfco  5767  omp1eomlem  7424  ltanqg  7757  genpassl  7881  genpassu  7882  ltexprlemloc  7964  caucvgprlemcanl  8001  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgprprlemaddq  8065  apneg  8929  lemuldiv  9201  msq11  9222  negiso  9275  avglt2  9524  xleaddadd  10268  iooshf  10333  qtri3or  10653  sq11ap  11123  hashen  11201  fihashdom  11221  cjap  11650  sqrt11ap  11782  mingeb  11986  xrnegiso  12006  clim2c  12028  climabs0  12051  absefib  12516  efieq1re  12517  nndivides  12542  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  halfleoddlt  12639  pc2dvds  13087  pcmpt  13100  issubm  13756  cnntr  15249  cndis  15265  cnpdis  15266  lmres  15272  txhmeo  15343  blininf  15448  cncfmet  15616