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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dfbi3dc  1386  xordidc  1388  19.32dc  1666  r19.32vdc  2613  opbrop  4677  fvopab3g  5553  respreima  5607  fmptco  5645  cocan1  5749  cocan2  5750  brtposg  6213  nnmword  6477  swoer  6520  erth  6536  brecop  6582  ecopovsymg  6591  xpdom2  6788  ctssdccl  7067  omniwomnimkv  7122  pitric  7253  ltexpi  7269  ltapig  7270  ltmpig  7271  ltanqg  7332  ltmnqg  7333  enq0breq  7368  genpassl  7456  genpassu  7457  1idprl  7522  1idpru  7523  caucvgprlemcanl  7576  ltasrg  7702  prsrlt  7719  caucvgsrlemoffcau  7730  ltpsrprg  7735  map2psrprg  7737  axpre-ltadd  7818  subsub23  8094  leadd1  8319  lemul1  8482  reapmul1lem  8483  reapmul1  8484  reapadd1  8485  apsym  8495  apadd1  8497  apti  8511  apcon4bid  8513  lediv1  8755  lt2mul2div  8765  lerec  8770  ltdiv2  8773  lediv2  8777  le2msq  8787  avgle1  9088  avgle2  9089  nn01to3  9546  qapne  9568  cnref1o  9579  xleneg  9764  xsubge0  9808  xleaddadd  9814  iooneg  9915  iccneg  9916  iccshftr  9921  iccshftl  9923  iccdil  9925  icccntr  9927  fzsplit2  9975  fzaddel  9984  fzrev  10009  elfzo  10074  fzon  10091  elfzom1b  10154  ioo0  10185  ico0  10187  ioc0  10188  flqlt  10208  negqmod0  10256  frec2uzled  10354  expeq0  10476  nn0leexp2  10613  nn0opthlem1d  10622  leisorel  10736  cjreb  10794  ltmininf  11162  minclpr  11164  xrmaxlesup  11186  xrltmininf  11197  xrminltinf  11199  tanaddaplem  11665  nndivdvds  11722  moddvds  11725  modmulconst  11749  oddm1even  11797  ltoddhalfle  11815  dvdssq  11949  phiprmpw  12131  eulerthlemh  12140  odzdvds  12154  pc2dvds  12238  cnrest2  12777  cnptoprest  12780  cnptoprest2  12781  lmss  12787  lmff  12790  txlm  12820  ismet2  12895  blres  12975  xmetec  12978  bdbl  13044  metrest  13047  cnbl0  13075  cnblcld  13076  reopnap  13079  bl2ioo  13083  limcdifap  13172  efle  13238  reapef  13240  logleb  13337  logrpap0b  13338  cxplt  13377  cxple  13378  rpcxple2  13379  rpcxplt2  13380  cxplt3  13381  cxple3  13382  apcxp2  13399  logbleb  13420  logblt  13421  iooref1o  13747