Theorem 3bitr4d 218

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 189	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 186	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  dfbi3dc  1328  xordidc  1330  19.32dc  1609  r19.32vdc  2503  opbrop  4437  fvopab3g  5266  respreima  5316  fmptco  5351  cocan1  5447  cocan2  5448  brtposg  5892  nnmword  6114  swoer  6157  erth  6173  brecop  6219  ecopovsymg  6228  xpdom2  6328  pitric  6511  ltexpi  6527  ltapig  6528  ltmpig  6529  ltanqg  6590  ltmnqg  6591  enq0breq  6626  genpassl  6714  genpassu  6715  1idprl  6780  1idpru  6781  caucvgprlemcanl  6834  ltasrg  6947  prsrlt  6963  caucvgsrlemoffcau  6974  axpre-ltadd  7052  subsub23  7313  leadd1  7534  lemul1  7693  reapmul1lem  7694  reapmul1  7695  reapadd1  7696  apsym  7706  apadd1  7708  apti  7722  lediv1  7947  lt2mul2div  7957  lerec  7962  ltdiv2  7965  lediv2  7969  le2msq  7979  avgle1  8271  avgle2  8272  nn01to3  8702  qapne  8724  cnref1o  8733  xleneg  8904  iooneg  9010  iccneg  9011  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzsplit2  9069  fzaddel  9077  fzrev  9101  elfzo  9159  fzon  9175  elfzom1b  9238  ioo0  9268  ico0  9270  ioc0  9271  flqlt  9285  negqmod0  9333  expeq0  9507  nn0opthlem1d  9647  cjreb  9753  abs00  9950  ltmininf  10116  nndivdvds  10201  moddvds  10204  modmulconst  10227  oddm1even  10274  ltoddhalfle  10293  dvdssq  10420