Theorem 3bitr4d 209

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (φ → (ψ ↔ χ))
3bitr4d.2	⊢ (φ → (θ ↔ ψ))
3bitr4d.3	⊢ (φ → (τ ↔ χ))

Assertion

Ref	Expression
3bitr4d	⊢ (φ → (θ ↔ τ))

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (φ → (θ ↔ ψ))
2		3bitr4d.1	. . 3 ⊢ (φ → (ψ ↔ χ))
3		3bitr4d.3	. . 3 ⊢ (φ → (τ ↔ χ))
4	2, 3	bitr4d 180	. 2 ⊢ (φ → (ψ ↔ τ))
5	1, 4	bitrd 177	1 ⊢ (φ → (θ ↔ τ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  dfbi3dc  1269  xordidc  1271  19.32dc  1547  r19.32vdc  2433  r19.12sn  3406  opbrop  4342  fvopab3g  5166  respreima  5216  fmptco  5251  cocan1  5348  cocan2  5349  brtposg  5787  nnmword  5998  swoer  6041  erth  6057  brecop  6103  ecopovsymg  6112  pitric  6175  ltexpi  6191  ltapig  6192  ltmpig  6193  ltanqg  6253  ltmnqg  6254  enq0breq  6285  genpassl  6373  genpassu  6374  1idprl  6423  1idpru  6424  ltasrg  6511  axpre-ltadd  6573  subsub23  6803  leadd1  7010