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  991  dfbi3dc  1439  xordidc  1441  19.32dc  1725  r19.32vdc  2680  opbrop  4803  fvopab3g  5715  respreima  5771  fmptco  5809  cocan1  5923  cocan2  5924  brtposg  6415  nnmword  6681  swoer  6725  erth  6743  brecop  6789  ecopovsymg  6798  xpdom2  7010  pw2f1odclem  7015  opabfi  7126  ctssdccl  7304  omniwomnimkv  7360  nninfwlporlemd  7365  pitric  7534  ltexpi  7550  ltapig  7551  ltmpig  7552  ltanqg  7613  ltmnqg  7614  enq0breq  7649  genpassl  7737  genpassu  7738  1idprl  7803  1idpru  7804  caucvgprlemcanl  7857  ltasrg  7983  prsrlt  8000  caucvgsrlemoffcau  8011  ltpsrprg  8016  map2psrprg  8018  axpre-ltadd  8099  subsub23  8377  leadd1  8603  lemul1  8766  reapmul1lem  8767  reapmul1  8768  reapadd1  8769  apsym  8779  apadd1  8781  apti  8795  apcon4bid  8797  lediv1  9042  lt2mul2div  9052  lerec  9057  ltdiv2  9060  lediv2  9064  le2msq  9074  avgle1  9378  avgle2  9379  nn01to3  9844  qapne  9866  cnref1o  9878  xleneg  10065  xsubge0  10109  xleaddadd  10115  iooneg  10216  iccneg  10217  iccshftr  10222  iccshftl  10224  iccdil  10226  icccntr  10228  fzsplit2  10278  fzaddel  10287  fzrev  10312  elfzo  10377  nelfzo  10380  fzon  10395  elfzom1b  10467  ioo0  10512  ico0  10514  ioc0  10515  flqlt  10536  negqmod0  10586  frec2uzled  10684  expeq0  10825  nn0leexp2  10965  nn0opthlem1d  10975  leisorel  11094  cjreb  11420  ltmininf  11789  minclpr  11791  xrmaxlesup  11813  xrltmininf  11824  xrminltinf  11826  tanaddaplem  12292  nndivdvds  12350  moddvds  12353  modmulconst  12377  oddm1even  12429  ltoddhalfle  12447  bitsp1  12505  dvdssq  12595  phiprmpw  12787  eulerthlemh  12796  odzdvds  12811  pc2dvds  12896  1arith  12933  issubg3  13772  eqgid  13806  resghm2b  13842  conjghm  13856  conjnmzb  13860  ablsubsub23  13905  issrgid  13987  isringid  14031  opprsubgg  14090  opprunitd  14117  crngunit  14118  unitpropdg  14155  issubrng  14206  opprsubrngg  14218  lsslss  14388  lsspropdg  14438  rspsn  14541  znidom  14664  cnrest2  14953  cnptoprest  14956  cnptoprest2  14957  lmss  14963  lmff  14966  txlm  14996  ismet2  15071  blres  15151  xmetec  15154  bdbl  15220  metrest  15223  cnbl0  15251  cnblcld  15252  reopnap  15263  bl2ioo  15267  limcdifap  15379  efle  15493  reapef  15495  logleb  15592  logrpap0b  15593  cxplt  15633  cxple  15634  rpcxple2  15635  rpcxplt2  15636  cxplt3  15637  cxple3  15638  apcxp2  15656  logbleb  15678  logblt  15679  lgsdilem  15749  lgsne0  15760  lgsquadlem1  15799  lgsquadlem2  15800  m1lgs  15807  2lgslem1a  15810  2lgs  15826  ausgrusgrben  16012  uspgr2wlkeq  16176  isclwwlknx  16225  iooref1o  16588