Theorem 3bitr4d 213

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

Syntax hints:   → wi 4   ↔ wb 102

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

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  dfbi3dc  1304  xordidc  1306  19.32dc  1585  r19.32vdc  2476  r19.12sn  3463  opbrop  4446  fvopab3g  5272  respreima  5322  fmptco  5357  cocan1  5454  cocan2  5455  brtposg  5899  nnmword  6121  swoer  6164  erth  6180  brecop  6226  ecopovsymg  6235  xpdom2  6335  pitric  6476  ltexpi  6492  ltapig  6493  ltmpig  6494  ltanqg  6555  ltmnqg  6556  enq0breq  6591  genpassl  6679  genpassu  6680  1idprl  6745  1idpru  6746  caucvgprlemcanl  6799  ltasrg  6912  prsrlt  6928  caucvgsrlemoffcau  6939  axpre-ltadd  7017  subsub23  7278  leadd1  7498  lemul1  7657  reapmul1lem  7658  reapmul1  7659  reapadd1  7660  apsym  7670  apadd1  7672  apti  7686  lediv1  7909  lt2mul2div  7919  lerec  7924  ltdiv2  7927  lediv2  7931  le2msq  7941  avgle1  8221  avgle2  8222  nn01to3  8648  qapne  8670  cnref1o  8679  xleneg  8850  iooneg  8956  iccneg  8957  iccshftr  8962  iccshftl  8964  iccdil  8966  icccntr  8968  fzsplit2  9015  fzaddel  9023  fzrev  9047  elfzo  9107  fzon  9123  elfzom1b  9186  flqlt  9227  negqmod0  9275  expeq0  9445  nn0opthlem1d  9581  cjreb  9687  abs00  9883  nndivdvds  10106  moddvds  10109  modmulconst  10131  oddm1even  10178  ltoddhalfle  10197