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  5088  dmfco  5632  omp1eomlem  7169  ltanqg  7484  genpassl  7608  genpassu  7609  ltexprlemloc  7691  caucvgprlemcanl  7728  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  caucvgprprlemaddq  7792  apneg  8655  lemuldiv  8925  msq11  8946  negiso  8999  avglt2  9248  xleaddadd  9979  iooshf  10044  qtri3or  10347  sq11ap  10816  hashen  10893  fihashdom  10912  cjap  11088  sqrt11ap  11220  mingeb  11424  xrnegiso  11444  clim2c  11466  climabs0  11489  absefib  11953  efieq1re  11954  nndivides  11979  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  halfleoddlt  12076  pc2dvds  12524  pcmpt  12537  issubm  13174  cnntr  14545  cndis  14561  cnpdis  14562  lmres  14568  txhmeo  14639  blininf  14744  cncfmet  14912