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  5154  dmfco  5714  omp1eomlem  7292  ltanqg  7619  genpassl  7743  genpassu  7744  ltexprlemloc  7826  caucvgprlemcanl  7863  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgprprlemaddq  7927  apneg  8790  lemuldiv  9060  msq11  9081  negiso  9134  avglt2  9383  xleaddadd  10121  iooshf  10186  qtri3or  10499  sq11ap  10968  hashen  11045  fihashdom  11065  cjap  11466  sqrt11ap  11598  mingeb  11802  xrnegiso  11822  clim2c  11844  climabs0  11867  absefib  12331  efieq1re  12332  nndivides  12357  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  halfleoddlt  12454  pc2dvds  12902  pcmpt  12915  issubm  13554  cnntr  14948  cndis  14964  cnpdis  14965  lmres  14971  txhmeo  15042  blininf  15147  cncfmet  15315