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  1329  xordidc  1331  19.32dc  1610  r19.32vdc  2508  opbrop  4465  fvopab3g  5297  respreima  5347  fmptco  5382  cocan1  5478  cocan2  5479  brtposg  5923  nnmword  6178  swoer  6221  erth  6237  brecop  6283  ecopovsymg  6292  xpdom2  6396  pitric  6625  ltexpi  6641  ltapig  6642  ltmpig  6643  ltanqg  6704  ltmnqg  6705  enq0breq  6740  genpassl  6828  genpassu  6829  1idprl  6894  1idpru  6895  caucvgprlemcanl  6948  ltasrg  7061  prsrlt  7077  caucvgsrlemoffcau  7088  axpre-ltadd  7166  subsub23  7432  leadd1  7653  lemul1  7812  reapmul1lem  7813  reapmul1  7814  reapadd1  7815  apsym  7825  apadd1  7827  apti  7841  lediv1  8066  lt2mul2div  8076  lerec  8081  ltdiv2  8084  lediv2  8088  le2msq  8098  avgle1  8390  avgle2  8391  nn01to3  8835  qapne  8857  cnref1o  8866  xleneg  9032  iooneg  9138  iccneg  9139  iccshftr  9144  iccshftl  9146  iccdil  9148  icccntr  9150  fzsplit2  9197  fzaddel  9205  fzrev  9229  elfzo  9288  fzon  9304  elfzom1b  9367  ioo0  9398  ico0  9400  ioc0  9401  flqlt  9417  negqmod0  9465  frec2uzled  9563  expeq0  9656  nn0opthlem1d  9796  cjreb  9954  abs00  10151  ltmininf  10317  nndivdvds  10409  moddvds  10412  modmulconst  10435  oddm1even  10482  ltoddhalfle  10500  dvdssq  10627  phiprmpw  10805