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  993  dfbi3dc  1441  xordidc  1443  19.32dc  1727  r19.32vdc  2682  opbrop  4805  fvopab3g  5719  respreima  5775  fmptco  5813  cocan1  5928  cocan2  5929  brtposg  6420  nnmword  6686  swoer  6730  erth  6748  brecop  6794  ecopovsymg  6803  xpdom2  7015  pw2f1odclem  7020  opabfi  7132  ctssdccl  7310  omniwomnimkv  7366  nninfwlporlemd  7371  pitric  7541  ltexpi  7557  ltapig  7558  ltmpig  7559  ltanqg  7620  ltmnqg  7621  enq0breq  7656  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  caucvgprlemcanl  7864  ltasrg  7990  prsrlt  8007  caucvgsrlemoffcau  8018  ltpsrprg  8023  map2psrprg  8025  axpre-ltadd  8106  subsub23  8384  leadd1  8610  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  apsym  8786  apadd1  8788  apti  8802  apcon4bid  8804  lediv1  9049  lt2mul2div  9059  lerec  9064  ltdiv2  9067  lediv2  9071  le2msq  9081  avgle1  9385  avgle2  9386  nn01to3  9851  qapne  9873  cnref1o  9885  xleneg  10072  xsubge0  10116  xleaddadd  10122  iooneg  10223  iccneg  10224  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzsplit2  10285  fzaddel  10294  fzrev  10319  elfzo  10384  nelfzo  10387  fzon  10402  elfzom1b  10475  ioo0  10520  ico0  10522  ioc0  10523  flqlt  10544  negqmod0  10594  frec2uzled  10692  expeq0  10833  nn0leexp2  10973  nn0opthlem1d  10983  leisorel  11102  cjreb  11431  ltmininf  11800  minclpr  11802  xrmaxlesup  11824  xrltmininf  11835  xrminltinf  11837  tanaddaplem  12304  nndivdvds  12362  moddvds  12365  modmulconst  12389  oddm1even  12441  ltoddhalfle  12459  bitsp1  12517  dvdssq  12607  phiprmpw  12799  eulerthlemh  12808  odzdvds  12823  pc2dvds  12908  1arith  12945  issubg3  13784  eqgid  13818  resghm2b  13854  conjghm  13868  conjnmzb  13872  ablsubsub23  13917  issrgid  14000  isringid  14044  opprsubgg  14103  opprunitd  14130  crngunit  14131  unitpropdg  14168  issubrng  14219  opprsubrngg  14231  lsslss  14401  lsspropdg  14451  rspsn  14554  znidom  14677  cnrest2  14966  cnptoprest  14969  cnptoprest2  14970  lmss  14976  lmff  14979  txlm  15009  ismet2  15084  blres  15164  xmetec  15167  bdbl  15233  metrest  15236  cnbl0  15264  cnblcld  15265  reopnap  15276  bl2ioo  15280  limcdifap  15392  efle  15506  reapef  15508  logleb  15605  logrpap0b  15606  cxplt  15646  cxple  15647  rpcxple2  15648  rpcxplt2  15649  cxplt3  15650  cxple3  15651  apcxp2  15669  logbleb  15691  logblt  15692  lgsdilem  15762  lgsne0  15773  lgsquadlem1  15812  lgsquadlem2  15813  m1lgs  15820  2lgslem1a  15823  2lgs  15839  ausgrusgrben  16025  uspgr2wlkeq  16222  isclwwlknx  16273  eupth2lem3lem6fi  16328  iooref1o  16664