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  1392  xordidc  1394  19.32dc  1672  r19.32vdc  2619  opbrop  4688  fvopab3g  5567  respreima  5621  fmptco  5659  cocan1  5763  cocan2  5764  brtposg  6230  nnmword  6494  swoer  6537  erth  6553  brecop  6599  ecopovsymg  6608  xpdom2  6805  ctssdccl  7084  omniwomnimkv  7139  pitric  7270  ltexpi  7286  ltapig  7287  ltmpig  7288  ltanqg  7349  ltmnqg  7350  enq0breq  7385  genpassl  7473  genpassu  7474  1idprl  7539  1idpru  7540  caucvgprlemcanl  7593  ltasrg  7719  prsrlt  7736  caucvgsrlemoffcau  7747  ltpsrprg  7752  map2psrprg  7754  axpre-ltadd  7835  subsub23  8111  leadd1  8336  lemul1  8499  reapmul1lem  8500  reapmul1  8501  reapadd1  8502  apsym  8512  apadd1  8514  apti  8528  apcon4bid  8530  lediv1  8772  lt2mul2div  8782  lerec  8787  ltdiv2  8790  lediv2  8794  le2msq  8804  avgle1  9105  avgle2  9106  nn01to3  9563  qapne  9585  cnref1o  9596  xleneg  9781  xsubge0  9825  xleaddadd  9831  iooneg  9932  iccneg  9933  iccshftr  9938  iccshftl  9940  iccdil  9942  icccntr  9944  fzsplit2  9993  fzaddel  10002  fzrev  10027  elfzo  10092  fzon  10109  elfzom1b  10172  ioo0  10203  ico0  10205  ioc0  10206  flqlt  10226  negqmod0  10274  frec2uzled  10372  expeq0  10494  nn0leexp2  10632  nn0opthlem1d  10641  leisorel  10759  cjreb  10817  ltmininf  11185  minclpr  11187  xrmaxlesup  11209  xrltmininf  11220  xrminltinf  11222  tanaddaplem  11688  nndivdvds  11745  moddvds  11748  modmulconst  11772  oddm1even  11821  ltoddhalfle  11839  dvdssq  11973  phiprmpw  12163  eulerthlemh  12172  odzdvds  12186  pc2dvds  12270  1arith  12306  cnrest2  12989  cnptoprest  12992  cnptoprest2  12993  lmss  12999  lmff  13002  txlm  13032  ismet2  13107  blres  13187  xmetec  13190  bdbl  13256  metrest  13259  cnbl0  13287  cnblcld  13288  reopnap  13291  bl2ioo  13295  limcdifap  13384  efle  13450  reapef  13452  logleb  13549  logrpap0b  13550  cxplt  13589  cxple  13590  rpcxple2  13591  rpcxplt2  13592  cxplt3  13593  cxple3  13594  apcxp2  13611  logbleb  13632  logblt  13633  lgsdilem  13681  lgsne0  13692  iooref1o  14026