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  1285  xordidc  1287  19.32dc  1566  r19.32vdc  2453  r19.12sn  3427  opbrop  4362  fvopab3g  5188  respreima  5238  fmptco  5273  cocan1  5370  cocan2  5371  brtposg  5810  nnmword  6027  swoer  6070  erth  6086  brecop  6132  ecopovsymg  6141  xpdom2  6241  pitric  6305  ltexpi  6321  ltapig  6322  ltmpig  6323  ltanqg  6384  ltmnqg  6385  enq0breq  6419  genpassl  6507  genpassu  6508  1idprl  6566  1idpru  6567  cauappcvgprlemcan  6616  ltasrg  6698  axpre-ltadd  6770  subsub23  7013  leadd1  7220  lemul1  7377  reapmul1lem  7378  reapmul1  7379  reapadd1  7380  apsym  7390  apadd1  7392  apti  7406  lediv1  7616  lt2mul2div  7626  lerec  7631  ltdiv2  7634  lediv2  7638  le2msq  7648  avgle1  7942  avgle2  7943  nn01to3  8328  qapne  8350  cnref1o  8357  xleneg  8520  iooneg  8626  iccneg  8627  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  fzsplit2  8684  fzaddel  8692  fzrev  8716  elfzo  8776  fzon  8792  elfzom1b  8855  expeq0  8940  cjreb  9094