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:  ifpdfbidc  994  dfbi3dc  1442  xordidc  1444  19.32dc  1727  r19.32vdc  2692  opbrop  4828  fvopab3g  5749  respreima  5804  fmptco  5842  cocan1  5959  cocan2  5960  suppimacnvfn  6445  brtposg  6484  nnmword  6750  swoer  6794  erth  6812  brecop  6858  ecopovsymg  6867  xpdom2  7081  pw2f1odclem  7086  opabfi  7199  ctssdccl  7401  omniwomnimkv  7457  nninfwlporlemd  7462  pitric  7635  ltexpi  7651  ltapig  7652  ltmpig  7653  ltanqg  7714  ltmnqg  7715  enq0breq  7750  genpassl  7838  genpassu  7839  1idprl  7904  1idpru  7905  caucvgprlemcanl  7958  ltasrg  8084  prsrlt  8101  caucvgsrlemoffcau  8112  ltpsrprg  8117  map2psrprg  8119  axpre-ltadd  8200  subsub23  8477  leadd1  8703  lemul1  8866  reapmul1lem  8867  reapmul1  8868  reapadd1  8869  apsym  8879  apadd1  8881  apti  8895  apcon4bid  8897  lediv1  9142  lt2mul2div  9152  lerec  9157  ltdiv2  9160  lediv2  9164  le2msq  9174  avgle1  9478  avgle2  9479  nn01to3  9948  qapne  9970  cnref1o  9982  xleneg  10169  xsubge0  10213  xleaddadd  10219  iooneg  10320  iccneg  10321  iccshftr  10326  iccshftl  10328  iccdil  10330  icccntr  10332  fzsplit2  10383  fzaddel  10392  fzrev  10417  elfzo  10482  nelfzo  10485  fzon  10500  elfzom1b  10573  ioo0  10618  ico0  10620  ioc0  10621  flqlt  10642  negqmod0  10692  frec2uzled  10790  expeq0  10931  nn0leexp2  11071  nn0opthlem1d  11081  leisorel  11205  cjreb  11547  ltmininf  11916  minclpr  11918  xrmaxlesup  11940  xrltmininf  11951  xrminltinf  11953  tanaddaplem  12420  nndivdvds  12478  moddvds  12481  modmulconst  12505  oddm1even  12557  ltoddhalfle  12575  bitsp1  12633  dvdssq  12723  phiprmpw  12915  eulerthlemh  12924  odzdvds  12939  pc2dvds  13024  1arith  13061  issubg3  13901  eqgid  13935  resghm2b  13971  conjghm  13985  conjnmzb  13989  ablsubsub23  14034  issrgid  14117  isringid  14161  opprsubgg  14220  opprunitd  14247  crngunit  14248  unitpropdg  14285  issubrng  14336  opprsubrngg  14348  lsslss  14521  lsspropdg  14571  rspsn  14674  znidom  14797  psrbagconf1o  14820  cnrest2  15093  cnptoprest  15096  cnptoprest2  15097  lmss  15103  lmff  15106  txlm  15136  ismet2  15211  blres  15291  xmetec  15294  bdbl  15360  metrest  15363  cnbl0  15391  cnblcld  15392  reopnap  15403  bl2ioo  15407  limcdifap  15519  efle  15633  reapef  15635  logleb  15732  logrpap0b  15733  cxplt  15773  cxple  15774  rpcxple2  15775  rpcxplt2  15776  cxplt3  15777  cxple3  15778  apcxp2  15796  logbleb  15818  logblt  15819  lgsdilem  15892  lgsne0  15903  lgsquadlem1  15942  lgsquadlem2  15943  m1lgs  15950  2lgslem1a  15953  2lgs  15969  ausgrusgrben  16155  uspgr2wlkeq  16352  isclwwlknx  16403  eupth2lem3lem6fi  16458  iooref1o  16810