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  suppinisegdc  6513  brtposg  6530  nnmword  6796  swoer  6840  erth  6858  brecop  6904  ecopovsymg  6913  xpdom2  7135  pw2f1odclem  7140  opabfi  7253  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  10033  qapne  10055  cnref1o  10068  xleneg  10256  xsubge0  10300  xleaddadd  10306  iooneg  10407  iccneg  10408  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzsplit2  10472  fzaddel  10482  fzrev  10508  elfzo  10573  nelfzo  10576  fzon  10591  elfzom1b  10664  ioo0  10711  ico0  10713  ioc0  10714  flqlt  10738  negqmod0  10789  frec2uzled  10887  expeq0  11028  nn0leexp2  11170  nn0opthlem1d  11180  leisorel  11311  cjreb  11653  ltmininf  12025  minclpr  12027  xrmaxlesup  12050  xrltmininf  12061  xrminltinf  12063  tanaddaplem  12530  nndivdvds  12588  moddvds  12591  modmulconst  12615  oddm1even  12667  ltoddhalfle  12685  bitsp1  12743  dvdssq  12833  phiprmpw  13029  eulerthlemh  13038  odzdvds  13053  pc2dvds  13138  1arith  13175  issubg3  14054  eqgid  14088  resghm2b  14124  conjghm  14138  conjnmzb  14142  resscntz  14166  cntzrec  14169  ablsubsub23  14219  issrgid  14392  isringid  14437  opprsubgg  14499  opprunitd  14526  crngunit  14527  unitpropdg  14564  issubrng  14616  opprsubrngg  14628  opprdrng  14729  lsslss  14827  lsspropdg  14877  rspsn  14980  znidom  15101  psrbagconf1o  15177  gsumbagdiaglem  15194  cnrest2  15495  cnptoprest  15498  cnptoprest2  15499  lmss  15505  lmff  15508  txlm  15538  ismet2  15613  blres  15693  xmetec  15696  bdbl  15762  metrest  15765  cnbl0  15793  cnblcld  15794  reopnap  15805  bl2ioo  15809  limcdifap  15921  efle  16035  reapef  16037  logleb  16138  logrpap0b  16139  logdivle  16158  cxplt  16184  cxple  16185  rpcxple2  16186  rpcxplt2  16187  cxplt3  16188  cxple3  16189  apcxp2  16207  logbleb  16230  logblt  16231  lgsdilem  16384  lgsne0  16395  lgsquadlem1  16434  lgsquadlem2  16435  m1lgs  16442  2lgslem1a  16445  2lgs  16461  ausgrusgrben  16647  uspgr2wlkeq  16844  isclwwlknx  16895  eupth2lem3lem6fi  16950  iooref1o  17322