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  1375  xordidc  1377  19.32dc  1657  r19.32vdc  2578  opbrop  4613  fvopab3g  5487  respreima  5541  fmptco  5579  cocan1  5681  cocan2  5682  brtposg  6144  nnmword  6407  swoer  6450  erth  6466  brecop  6512  ecopovsymg  6521  xpdom2  6718  ctssdccl  6989  pitric  7122  ltexpi  7138  ltapig  7139  ltmpig  7140  ltanqg  7201  ltmnqg  7202  enq0breq  7237  genpassl  7325  genpassu  7326  1idprl  7391  1idpru  7392  caucvgprlemcanl  7445  ltasrg  7571  prsrlt  7588  caucvgsrlemoffcau  7599  ltpsrprg  7604  map2psrprg  7606  axpre-ltadd  7687  subsub23  7960  leadd1  8185  lemul1  8348  reapmul1lem  8349  reapmul1  8350  reapadd1  8351  apsym  8361  apadd1  8363  apti  8377  apcon4bid  8379  lediv1  8620  lt2mul2div  8630  lerec  8635  ltdiv2  8638  lediv2  8642  le2msq  8652  avgle1  8953  avgle2  8954  nn01to3  9402  qapne  9424  cnref1o  9433  xleneg  9613  xsubge0  9657  xleaddadd  9663  iooneg  9764  iccneg  9765  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  fzsplit2  9823  fzaddel  9832  fzrev  9857  elfzo  9919  fzon  9936  elfzom1b  9999  ioo0  10030  ico0  10032  ioc0  10033  flqlt  10049  negqmod0  10097  frec2uzled  10195  expeq0  10317  nn0opthlem1d  10459  leisorel  10573  cjreb  10631  ltmininf  10999  minclpr  11001  xrmaxlesup  11021  xrltmininf  11032  xrminltinf  11034  tanaddaplem  11434  nndivdvds  11488  moddvds  11491  modmulconst  11514  oddm1even  11561  ltoddhalfle  11579  dvdssq  11708  phiprmpw  11887  cnrest2  12394  cnptoprest  12397  cnptoprest2  12398  lmss  12404  lmff  12407  txlm  12437  ismet2  12512  blres  12592  xmetec  12595  bdbl  12661  metrest  12664  cnbl0  12692  cnblcld  12693  reopnap  12696  bl2ioo  12700  limcdifap  12789