Theorem 3bitr4d 313

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 284	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 281	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  pr1eqbg  4780  fvopab3g  6757  fvimacnvALT  6821  respreima  6830  fmptco  6885  fnnfpeq0  6934  cocan1  7041  cocan2  7042  ordsucelsuc  7531  ordsucsssuc  7532  fnsuppres  7851  smoword  7997  oaword  8169  omword  8190  om00el  8196  oeword  8210  nnaword  8247  nnmword  8253  swoer  8313  erth  8332  brecop  8384  eceqoveq  8396  xpdom2  8606  pw2f1olem  8615  ixpfi2  8816  cantnfrescl  9133  rankr1bg  9226  r1pwcl  9270  fseqenlem1  9444  alephord3  9498  alephdom2  9507  engch  10044  fpwwe2lem7  10052  fpwwe2lem9  10054  ltexpi  10318  ltapi  10319  ltmpi  10320  ltsonq  10385  ltmnq  10388  1idpr  10445  addcanpr  10462  axpre-ltadd  10583  axlttri  10706  subsub23  10885  leadd1  11102  ltsub1  11130  ltsub2  11131  leord1  11161  eqord1  11162  lemul1  11486  lediv1  11499  lt2mul2div  11512  lerec  11517  lediv2  11524  le2msq  11534  suprleub  11601  infregelb  11619  ofsubeq0  11629  ofsubge0  11631  avgle1  11871  avgle2  11872  cnref1o  12378  xleneg  12605  xnn0lem1lt  12631  xltadd1  12643  xsubge0  12648  xposdif  12649  xltmul1  12679  supxrleub  12713  infxrgelb  12722  iooneg  12851  iccneg  12852  iccsplit  12865  iccshftr  12866  iccshftl  12868  iccdil  12870  icccntr  12872  fzsplit2  12926  fzaddel  12935  fzrev  12964  predfz  13026  elfzo  13034  nelfzo  13037  fzon  13052  elfzom1b  13130  negmod0  13240  leexp2  13529  ltexp2r  13531  repswsymball  14135  repswsymballbi  14136  cjreb  14476  sqrtlt  14615  limsuplt  14830  o1lo1  14888  rlimresb  14916  lo1eq  14919  rlimeq  14920  o1eq  14921  isercoll  15018  efle  15465  tanaddlem  15513  nndivdvds  15610  moddvds  15612  modmulconst  15635  oddm1even  15686  ltoddhalfle  15704  bitsp1  15774  sadcaddlem  15800  sadadd  15810  sadass  15814  bitsshft  15818  smuval2  15825  smumul  15836  dvdssq  15905  phiprmpw  16107  eulerthlem2  16113  odzdvds  16126  pc2dvds  16209  1arith  16257  imasleval  16808  mreacs  16923  catpropd  16973  oppcsect  17042  funcres2b  17161  fthsect  17189  fthinv  17190  fucsect  17236  fucinv  17237  latnlemlt  17688  latnle  17689  ipole  17762  ipolt  17763  issubg3  18291  eqgid  18326  resghm2b  18370  conjghm  18383  gastacos  18434  resscntz  18456  cntzrec  18458  oppgsubm  18484  oppgsubg  18485  sylow3lem6  18751  lsmcom2  18774  lsmass  18789  ablsubsub23  18939  lsmcomx  18970  subgdmdprd  19150  opprsubrg  19550  lsslss  19727  lbspropd  19865  islbs2  19920  rspsn  20021  psrbagconf1o  20148  gsumbagdiaglem  20149  mplmonmul  20239  prmirred  20636  znfld  20701  lindfmm  20965  lindsmm  20966  lsslindf  20968  lsslinds  20969  islindf4  20976  basdif0  21555  neiptopreu  21735  neitr  21782  restlp  21785  cnrest2  21888  cnprest  21891  cnprest2  21892  lmss  21900  lmff  21903  ist1-2  21949  lpcls  21966  perfcls  21967  cmpfi  22010  hauseqlcld  22248  txlm  22250  txkgen  22254  xkopt  22257  idqtop  22308  tgqtop  22314  qtopcn  22316  uffix  22523  fmco  22563  flimrest  22585  lmflf  22607  txflf  22608  fclsrest  22626  cnpfcf  22643  tsmsgsum  22741  tsmsres  22746  tsmsf1o  22747  fmucndlem  22894  ismet2  22937  imasf1oxmet  22979  blres  23035  xmetec  23038  imasf1obl  23092  imasf1oxms  23093  prdsbl  23095  stdbdbl  23121  metrest  23128  metustsym  23159  blval2  23166  metuel2  23169  tngngp  23257  cnbl0  23376  cnblcld  23377  bl2ioo  23394  cncfcnvcn  23523  iihalf2  23531  icoopnst  23537  iocopnst  23538  icopnfcnv  23540  icopnfhmeo  23541  cphorthcom  23799  caucfil  23880  lmclim  23900  cmsss  23948  rrxmet  24005  volsup  24151  dyaddisjlem  24190  mbfeqalem1  24236  mbfeqalem2  24237  mbfeqa  24238  mbfmulc2lem  24242  mbfmax  24244  mbfposr  24247  ismbf3d  24249  mbfimaopnlem  24250  mbfaddlem  24255  mbfsup  24259  mbfinf  24260  0plef  24267  0pledm  24268  i1fmulclem  24297  i1fres  24300  i1fpos  24301  itg1climres  24309  mbfi1fseqlem4  24313  itg2mulclem  24341  itg2monolem1  24345  itg2cnlem1  24356  iblre  24388  iblcn  24393  itgeqa  24408  ellimc2  24469  limcflf  24473  dvreslem  24501  lhop1  24605  ply1remlem  24750  fta1glem2  24754  ofmulrt  24865  plydiveu  24881  plyremlem  24887  quotcan  24892  ulmres  24970  cos11  25111  logleb  25180  argrege0  25188  logdivle  25199  efopn  25235  logccv  25240  cxplt  25271  cxple  25272  cxple2  25274  cxplt2  25275  cxplt3  25277  cxple3  25278  logbleb  25355  logblt  25356  angrtmuld  25380  quad2  25411  atans2  25503  rlimcnp  25537  rlimcnp2  25538  rlimcxp  25545  sqff1o  25753  fsumvma2  25784  dchrptlem2  25835  lgsdilem  25894  lgsne0  25905  lgsqr  25921  lgsquadlem1  25950  lgsquadlem2  25951  m1lgs  25958  2lgslem1a  25961  2lgs  25977  dchrisum0lem1  26086  padicabv  26200  trgcgrg  26295  colcom  26338  colrot1  26339  ishlg  26382  hlcomb  26383  hlbtwn  26391  lncom  26402  lnrot2  26404  israg  26477  perpcom  26493  hpgcom  26547  colopp  26549  iscgra  26589  isinag  26618  colinearalglem2  26687  axcgrid  26696  uvtx01vtx  27173  iscplgredg  27193  rgrusgrprc  27365  uspgr2wlkeq  27421  clwlkclwwlk  27774  eupth2lem3lem6  28006  fusgr2wsp2nb  28107  nmorepnf  28539  blocnilem  28575  ubthlem1  28641  shscom  29090  pjpreeq  29169  spansncol  29339  cmcm2  29387  hodsi  29546  nmoprepnf  29638  nmfnrepnf  29651  pjssposi  29943  cvcon3  30055  mdsymlem8  30181  dmdsym  30184  disjunsn  30338  fimarab  30384  unipreima  30385  fmptcof2  30396  1stpreima  30436  fpwrelmapffslem  30462  infxrge0gelb  30484  nndiffz1  30503  cntzun  30690  isinftm  30805  qusxpid  30923  lindfpropd  30937  lindspropd  30938  finexttrb  31047  metidv  31127  metider  31129  pstmxmet  31132  xrge0iifiso  31173  indpi1  31274  prodindf  31277  indf1ofs  31280  aean  31498  brfae  31502  signsply0  31816  signsvfn  31847  reprinrn  31884  subfacp1lem3  32424  subfacp1lem5  32426  fmlafvel  32627  opelco3  33013  sscoid  33369  cgrcomr  33453  ofscom  33463  cgr3permute3  33503  cgr3permute1  33504  cgr3com  33509  colinearperm1  33518  colinearperm3  33519  outsideofcom  33584  opnbnd  33668  filnetlem4  33724  finxpsuclem  34672  wl-equsald  34773  lindsadd  34879  poimirlem23  34909  broucube  34920  heicant  34921  itg2addnclem2  34938  ftc1anclem1  34961  ftc1anclem5  34965  ftc1anclem6  34966  areacirclem5  34980  areacirc  34981  caures  35029  cnpwstotbnd  35069  ismtyima  35075  rrnmet  35101  reheibor  35111  rngosn3  35196  brcosscnvcoss  35673  br1cosscnvxrn  35708  eqvrelth  35840  lcvbr  36151  lkrsc  36227  lshpkrlem1  36240  opltcon3b  36334  cmt2N  36380  cmt3N  36381  cvrcon3b  36407  cvrcmp2  36414  cvlexchb2  36461  cvlatexchb2  36465  2llnmj  36690  4atlem3  36726  4atlem9  36733  4atlem10a  36734  4atlem11a  36737  4atlem12a  36740  4at2  36744  2lplnmj  36752  llnexchb2  36999  lautlt  37221  lautcvr  37222  lautco  37227  ltrnatb  37267  ltrneq2  37278  cdlemefrs29pre00  37525  cdlemefrs29cpre1  37528  cdleme32fva  37567  dibglbN  38296  dochsncom  38512  dochkrsat  38585  lspindp5  38900  mapdh8ab  38907  hdmapip0com  39047  prjsprellsp  39254  lzenom  39360  rmxycomplete  39507  fzneg  39572  modabsdifz  39576  jm2.19  39583  pw2f1ocnv  39627  brtrclfv2  40065  rfovcnvf1od  40343  ntrclsfveq1  40403  ntrclsiso  40410  k0004lem2  40491  caofcan  40648  rfcnpre1  41269  rfcnpre2  41281  ellimcabssub0  41891  liminfpnfuz  42090  xlimpnfxnegmnf2  42132  fperdvper  42196  vonvolmbl  42937  readdcnnred  43497  resubcnnred  43498  cndivrenred  43500  requad2  43782  mgmpropd  44036  lco0  44476  lindslininds  44513  ltsubaddb  44563  ltsubsubb  44564  ltsubadd2b  44565  elbigolo1  44611  dig2bits  44668  rrx2pnedifcoorneorr  44698