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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpdfbidc  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4856  fvopab3g  5781  respreima  5839  fmptco  5877  cocan1  5996  cocan2  5997  suppimacnvfn  6490  brtposg  6529  nnmword  6795  swoer  6839  erth  6857  brecop  6903  ecopovsymg  6912  xpdom2  7134  pw2f1odclem  7139  opabfi  7252  ctssdccl  7458  omniwomnimkv  7514  nninfwlporlemd  7519  pitric  7695  ltexpi  7711  ltapig  7712  ltmpig  7713  ltanqg  7774  ltmnqg  7775  enq0breq  7810  genpassl  7898  genpassu  7899  1idprl  7964  1idpru  7965  caucvgprlemcanl  8018  ltasrg  8144  prsrlt  8161  caucvgsrlemoffcau  8172  ltpsrprg  8177  map2psrprg  8179  axpre-ltadd  8260  subsub23  8539  leadd1  8766  lemul1  8930  reapmul1lem  8931  reapmul1  8932  reapadd1  8933  apsym  8943  apadd1  8945  apti  8959  apcon4bid  8961  lediv1  9208  lt2mul2div  9218  lerec  9223  ltdiv2  9226  lediv2  9230  le2msq  9240  ofsubeq0  9301  avgle1  9558  avgle2  9559  nn01to3  10034  qapne  10056  cnref1o  10069  xleneg  10257  xsubge0  10301  xleaddadd  10307  iooneg  10408  iccneg  10409  iccshftr  10414  iccshftl  10416  iccdil  10418  icccntr  10420  fzsplit2  10473  fzaddel  10483  fzrev  10509  elfzo  10574  nelfzo  10577  fzon  10592  elfzom1b  10665  ioo0  10712  ico0  10714  ioc0  10715  flqlt  10739  negqmod0  10790  frec2uzled  10888  expeq0  11029  nn0leexp2  11171  nn0opthlem1d  11181  leisorel  11312  cjreb  11654  ltmininf  12026  minclpr  12028  xrmaxlesup  12051  xrltmininf  12062  xrminltinf  12064  tanaddaplem  12531  nndivdvds  12589  moddvds  12592  modmulconst  12616  oddm1even  12668  ltoddhalfle  12686  bitsp1  12744  dvdssq  12834  phiprmpw  13030  eulerthlemh  13039  odzdvds  13054  pc2dvds  13139  1arith  13176  issubg3  14055  eqgid  14089  resghm2b  14125  conjghm  14139  conjnmzb  14143  resscntz  14167  cntzrec  14170  ablsubsub23  14220  issrgid  14393  isringid  14438  opprsubgg  14500  opprunitd  14527  crngunit  14528  unitpropdg  14565  issubrng  14617  opprsubrngg  14629  opprdrng  14730  lsslss  14828  lsspropdg  14878  rspsn  14981  znidom  15102  psrbagconf1o  15179  gsumbagdiaglem  15180  cnrest2  15474  cnptoprest  15477  cnptoprest2  15478  lmss  15484  lmff  15487  txlm  15517  ismet2  15592  blres  15672  xmetec  15675  bdbl  15741  metrest  15744  cnbl0  15772  cnblcld  15773  reopnap  15784  bl2ioo  15788  limcdifap  15900  efle  16014  reapef  16016  logleb  16117  logrpap0b  16118  logdivle  16137  cxplt  16163  cxple  16164  rpcxple2  16165  rpcxplt2  16166  cxplt3  16167  cxple3  16168  apcxp2  16186  logbleb  16209  logblt  16210  lgsdilem  16363  lgsne0  16374  lgsquadlem1  16413  lgsquadlem2  16414  m1lgs  16421  2lgslem1a  16424  2lgs  16440  ausgrusgrben  16626  uspgr2wlkeq  16823  isclwwlknx  16874  eupth2lem3lem6fi  16929  iooref1o  17301