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  6418  genpassl  6506  genpassu  6507  1idprl  6565  1idpru  6566  cauappcvgprlemcan  6615  ltasrg  6678  axpre-ltadd  6750  subsub23  6993  leadd1  7200  lemul1  7357  reapmul1lem  7358  reapmul1  7359  reapadd1  7360  apsym  7370  apadd1  7372  apti  7386  lediv1  7596  lt2mul2div  7606  lerec  7611  ltdiv2  7614  lediv2  7618  le2msq  7628  avgle1  7922  avgle2  7923  nn01to3  8308  qapne  8330  cnref1o  8337  xleneg  8500  iooneg  8606  iccneg  8607  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  fzsplit2  8664  fzaddel  8672  fzrev  8696  elfzo  8756  fzon  8772  elfzom1b  8835  expeq0  8920  cjreb  9074