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  5109  dmfco  5660  omp1eomlem  7211  ltanqg  7533  genpassl  7657  genpassu  7658  ltexprlemloc  7740  caucvgprlemcanl  7777  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  caucvgprprlemaddq  7841  apneg  8704  lemuldiv  8974  msq11  8995  negiso  9048  avglt2  9297  xleaddadd  10029  iooshf  10094  qtri3or  10405  sq11ap  10874  hashen  10951  fihashdom  10970  cjap  11292  sqrt11ap  11424  mingeb  11628  xrnegiso  11648  clim2c  11670  climabs0  11693  absefib  12157  efieq1re  12158  nndivides  12183  oddnn02np1  12266  oddge22np1  12267  evennn02n  12268  evennn2n  12269  halfleoddlt  12280  pc2dvds  12728  pcmpt  12741  issubm  13379  cnntr  14772  cndis  14788  cnpdis  14789  lmres  14795  txhmeo  14866  blininf  14971  cncfmet  15139