Theorem 3bitr4d 219

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dfbi3dc  1343  xordidc  1345  19.32dc  1625  r19.32vdc  2538  opbrop  4556  fvopab3g  5426  respreima  5480  fmptco  5518  cocan1  5620  cocan2  5621  brtposg  6081  nnmword  6344  swoer  6387  erth  6403  brecop  6449  ecopovsymg  6458  xpdom2  6654  ctssdclemr  6911  pitric  7030  ltexpi  7046  ltapig  7047  ltmpig  7048  ltanqg  7109  ltmnqg  7110  enq0breq  7145  genpassl  7233  genpassu  7234  1idprl  7299  1idpru  7300  caucvgprlemcanl  7353  ltasrg  7466  prsrlt  7482  caucvgsrlemoffcau  7493  axpre-ltadd  7571  subsub23  7838  leadd1  8059  lemul1  8221  reapmul1lem  8222  reapmul1  8223  reapadd1  8224  apsym  8234  apadd1  8236  apti  8250  apcon4bid  8252  lediv1  8485  lt2mul2div  8495  lerec  8500  ltdiv2  8503  lediv2  8507  le2msq  8517  avgle1  8812  avgle2  8813  nn01to3  9259  qapne  9281  cnref1o  9290  xleneg  9461  xsubge0  9505  xleaddadd  9511  iooneg  9612  iccneg  9613  iccshftr  9618  iccshftl  9620  iccdil  9622  icccntr  9624  fzsplit2  9671  fzaddel  9680  fzrev  9705  elfzo  9767  fzon  9784  elfzom1b  9847  ioo0  9878  ico0  9880  ioc0  9881  flqlt  9897  negqmod0  9945  frec2uzled  10043  expeq0  10165  nn0opthlem1d  10307  leisorel  10421  cjreb  10479  ltmininf  10845  minclpr  10847  xrmaxlesup  10867  xrltmininf  10878  xrminltinf  10880  tanaddaplem  11243  nndivdvds  11294  moddvds  11297  modmulconst  11320  oddm1even  11367  ltoddhalfle  11385  dvdssq  11512  phiprmpw  11690  cnrest2  12186  cnptoprest  12189  cnptoprest2  12190  lmss  12196  lmff  12199  txlm  12229  ismet2  12282  blres  12362  xmetec  12365  bdbl  12431  metrest  12434  cnbl0  12456  cnblcld  12457  bl2ioo  12461  limcdifap  12512