Theorem 3bitr4d 220

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dfbi3dc  1397  xordidc  1399  19.32dc  1679  r19.32vdc  2626  opbrop  4706  fvopab3g  5590  respreima  5645  fmptco  5683  cocan1  5788  cocan2  5789  brtposg  6255  nnmword  6519  swoer  6563  erth  6579  brecop  6625  ecopovsymg  6634  xpdom2  6831  ctssdccl  7110  omniwomnimkv  7165  nninfwlporlemd  7170  pitric  7320  ltexpi  7336  ltapig  7337  ltmpig  7338  ltanqg  7399  ltmnqg  7400  enq0breq  7435  genpassl  7523  genpassu  7524  1idprl  7589  1idpru  7590  caucvgprlemcanl  7643  ltasrg  7769  prsrlt  7786  caucvgsrlemoffcau  7797  ltpsrprg  7802  map2psrprg  7804  axpre-ltadd  7885  subsub23  8162  leadd1  8387  lemul1  8550  reapmul1lem  8551  reapmul1  8552  reapadd1  8553  apsym  8563  apadd1  8565  apti  8579  apcon4bid  8581  lediv1  8826  lt2mul2div  8836  lerec  8841  ltdiv2  8844  lediv2  8848  le2msq  8858  avgle1  9159  avgle2  9160  nn01to3  9617  qapne  9639  cnref1o  9650  xleneg  9837  xsubge0  9881  xleaddadd  9887  iooneg  9988  iccneg  9989  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzsplit2  10050  fzaddel  10059  fzrev  10084  elfzo  10149  fzon  10166  elfzom1b  10229  ioo0  10260  ico0  10262  ioc0  10263  flqlt  10283  negqmod0  10331  frec2uzled  10429  expeq0  10551  nn0leexp2  10690  nn0opthlem1d  10700  leisorel  10817  cjreb  10875  ltmininf  11243  minclpr  11245  xrmaxlesup  11267  xrltmininf  11278  xrminltinf  11280  tanaddaplem  11746  nndivdvds  11803  moddvds  11806  modmulconst  11830  oddm1even  11880  ltoddhalfle  11898  dvdssq  12032  phiprmpw  12222  eulerthlemh  12231  odzdvds  12245  pc2dvds  12329  1arith  12365  issubg3  13052  eqgid  13085  ablsubsub23  13128  issrgid  13164  isringid  13208  opprunitd  13279  crngunit  13280  unitpropdg  13317  cnrest2  13739  cnptoprest  13742  cnptoprest2  13743  lmss  13749  lmff  13752  txlm  13782  ismet2  13857  blres  13937  xmetec  13940  bdbl  14006  metrest  14009  cnbl0  14037  cnblcld  14038  reopnap  14041  bl2ioo  14045  limcdifap  14134  efle  14200  reapef  14202  logleb  14299  logrpap0b  14300  cxplt  14339  cxple  14340  rpcxple2  14341  rpcxplt2  14342  cxplt3  14343  cxple3  14344  apcxp2  14361  logbleb  14382  logblt  14383  lgsdilem  14431  lgsne0  14442  m1lgs  14455  iooref1o  14785