Theorem 3bitr4d 310

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pr1eqbg  4801  unisucg  6379  fvopab3g  6926  fvimacnvALT  6990  respreima  6999  fmptco  7057  fnnfpeq0  7106  cocan1  7219  cocan2  7220  ordsucelsuc  7735  ordsucsssuc  7736  fnsuppres  8077  smoword  8267  oaword  8451  omword  8472  om00el  8478  oeword  8492  nnaword  8529  nnmword  8535  eldifsucnn  8565  swoer  8599  erth  8618  brecop  8670  eceqoveq  8682  xpdom2  8932  pw2f1olem  8941  ixpfi2  9215  cantnfrescl  9533  ttrclselem2  9583  rankr1bg  9660  r1pwcl  9704  fseqenlem1  9881  alephord3  9935  alephdom2  9944  engch  10485  fpwwe2lem6  10493  fpwwe2lem8  10495  ltexpi  10759  ltapi  10760  ltmpi  10761  ltsonq  10826  ltmnq  10829  1idpr  10886  addcanpr  10903  axpre-ltadd  11024  axlttri  11147  subsub23  11327  leadd1  11544  ltsub1  11572  ltsub2  11573  leord1  11603  eqord1  11604  lemul1  11928  lediv1  11941  lt2mul2div  11954  lerec  11959  lediv2  11966  le2msq  11976  suprleub  12042  infregelb  12060  ofsubeq0  12071  ofsubge0  12073  avgle1  12314  avgle2  12315  cnref1o  12826  xleneg  13053  xnn0lem1lt  13079  xltadd1  13091  xsubge0  13096  xposdif  13097  xltmul1  13127  supxrleub  13161  infxrgelb  13170  iooneg  13304  iccneg  13305  iccsplit  13318  iccshftr  13319  iccshftl  13321  iccdil  13323  icccntr  13325  fzsplit2  13382  fzaddel  13391  fzrev  13420  predfz  13482  elfzo  13490  nelfzo  13493  fzon  13509  elfzom1b  13587  negmod0  13699  leexp2  13990  ltexp2r  13992  repswsymball  14590  repswsymballbi  14591  cjreb  14933  sqrtlt  15072  limsuplt  15287  o1lo1  15345  rlimresb  15373  lo1eq  15376  rlimeq  15377  o1eq  15378  isercoll  15478  efle  15926  tanaddlem  15974  nndivdvds  16071  moddvds  16073  modmulconst  16096  oddm1even  16151  ltoddhalfle  16169  bitsp1  16237  sadcaddlem  16263  sadadd  16273  sadass  16277  bitsshft  16281  smuval2  16288  smumul  16299  dvdssq  16369  phiprmpw  16574  eulerthlem2  16580  odzdvds  16593  pc2dvds  16677  1arith  16725  imasleval  17349  mreacs  17464  catpropd  17515  oppcsect  17587  funcres2b  17709  fthsect  17738  fthinv  17739  fucsect  17787  fucinv  17788  latnlemlt  18287  latnle  18288  ipole  18349  ipolt  18350  issubg3  18869  eqgid  18904  resghm2b  18948  conjghm  18961  gastacos  19012  resscntz  19034  cntzrec  19036  oppgsubm  19065  oppgsubg  19066  sylow3lem6  19333  lsmcom2  19356  lsmass  19370  ablsubsub23  19521  lsmcomx  19552  subgdmdprd  19732  opprsubrg  20150  lsslss  20329  lbspropd  20467  islbs2  20522  rspsn  20631  prmirred  20802  znfld  20874  lindfmm  21140  lindsmm  21141  lsslindf  21143  lsslinds  21144  islindf4  21151  psrbagconf1o  21245  psrbagconf1oOLD  21246  gsumbagdiaglemOLD  21247  gsumbagdiaglem  21250  mplmonmul  21343  basdif0  22209  neiptopreu  22390  neitr  22437  restlp  22440  cnrest2  22543  cnprest  22546  cnprest2  22547  lmss  22555  lmff  22558  ist1-2  22604  lpcls  22621  perfcls  22622  cmpfi  22665  hauseqlcld  22903  txlm  22905  txkgen  22909  xkopt  22912  idqtop  22963  tgqtop  22969  qtopcn  22971  uffix  23178  fmco  23218  flimrest  23240  lmflf  23262  txflf  23263  fclsrest  23281  cnpfcf  23298  tsmsgsum  23396  tsmsres  23401  tsmsf1o  23402  fmucndlem  23549  ismet2  23592  imasf1oxmet  23634  blres  23690  xmetec  23693  imasf1obl  23750  imasf1oxms  23751  prdsbl  23753  stdbdbl  23779  metrest  23786  metustsym  23817  blval2  23824  metuel2  23827  tngngp  23924  cnbl0  24043  cnblcld  24044  bl2ioo  24061  cncfcnvcn  24194  iihalf2  24202  icoopnst  24208  iocopnst  24209  icopnfcnv  24211  icopnfhmeo  24212  cphorthcom  24471  caucfil  24553  lmclim  24573  cmsss  24621  rrxmet  24678  volsup  24826  dyaddisjlem  24865  mbfeqalem1  24911  mbfeqalem2  24912  mbfeqa  24913  mbfmulc2lem  24917  mbfmax  24919  mbfposr  24922  ismbf3d  24924  mbfimaopnlem  24925  mbfaddlem  24930  mbfsup  24934  mbfinf  24935  0plef  24942  0pledm  24943  i1fmulclem  24973  i1fres  24976  i1fpos  24977  itg1climres  24985  mbfi1fseqlem4  24989  itg2mulclem  25017  itg2monolem1  25021  itg2cnlem1  25032  iblre  25064  iblcn  25069  itgeqa  25084  ellimc2  25147  limcflf  25151  dvreslem  25179  lhop1  25284  ply1remlem  25433  fta1glem2  25437  ofmulrt  25548  plydiveu  25564  plyremlem  25570  quotcan  25575  ulmres  25653  cos11  25795  logleb  25864  argrege0  25872  logdivle  25883  efopn  25919  logccv  25924  cxplt  25955  cxple  25956  cxple2  25958  cxplt2  25959  cxplt3  25961  cxple3  25962  logbleb  26039  logblt  26040  angrtmuld  26064  quad2  26095  atans2  26187  rlimcnp  26221  rlimcnp2  26222  rlimcxp  26229  sqff1o  26437  fsumvma2  26468  dchrptlem2  26519  lgsdilem  26578  lgsne0  26589  lgsqr  26605  lgsquadlem1  26634  lgsquadlem2  26635  m1lgs  26642  2lgslem1a  26645  2lgs  26661  dchrisum0lem1  26770  padicabv  26884  nosupinfsep  26986  trgcgrg  27165  colcom  27208  colrot1  27209  ishlg  27252  hlcomb  27253  hlbtwn  27261  lncom  27272  lnrot2  27274  israg  27347  perpcom  27363  hpgcom  27417  colopp  27419  iscgra  27459  isinag  27488  colinearalglem2  27564  axcgrid  27573  uvtx01vtx  28053  iscplgredg  28073  rgrusgrprc  28245  uspgr2wlkeq  28302  clwlkclwwlk  28654  eupth2lem3lem6  28885  fusgr2wsp2nb  28986  nmorepnf  29418  blocnilem  29454  ubthlem1  29520  shscom  29969  pjpreeq  30048  spansncol  30218  cmcm2  30266  hodsi  30425  nmoprepnf  30517  nmfnrepnf  30530  pjssposi  30822  cvcon3  30934  mdsymlem8  31060  dmdsym  31063  disjunsn  31220  fimarab  31267  unipreima  31268  fmptcof2  31281  ressupprn  31311  1stpreima  31326  fpwrelmapffslem  31354  infxrge0gelb  31376  nndiffz1  31394  mgccnv  31564  pwrssmgc  31565  cntzun  31607  isinftm  31722  qusxpid  31855  lindfpropd  31873  lindspropd  31874  lsmssass  31887  nsgmgc  31894  finexttrb  32035  ist0cld  32081  metidv  32140  metider  32142  pstmxmet  32145  xrge0iifiso  32183  indpi1  32286  prodindf  32289  indf1ofs  32292  aean  32510  brfae  32514  signsply0  32830  signsvfn  32861  reprinrn  32898  subfacp1lem3  33443  subfacp1lem5  33445  fmlafvel  33646  opelco3  34032  naddss1  34120  oldlim  34165  newbday  34178  sscoid  34311  cgrcomr  34395  ofscom  34405  cgr3permute3  34445  cgr3permute1  34446  cgr3com  34451  colinearperm1  34460  colinearperm3  34461  outsideofcom  34526  opnbnd  34610  filnetlem4  34666  finxpsuclem  35673  wl-equsald  35803  lindsadd  35875  poimirlem23  35905  broucube  35916  heicant  35917  itg2addnclem2  35934  ftc1anclem1  35955  ftc1anclem5  35959  ftc1anclem6  35960  areacirclem5  35974  areacirc  35975  caures  36023  cnpwstotbnd  36060  ismtyima  36066  rrnmet  36092  reheibor  36102  rngosn3  36187  brcosscnvcoss  36701  br1cosscnvxrn  36741  eqvrelth  36878  brpartspart  37040  lcvbr  37288  lkrsc  37364  lshpkrlem1  37377  opltcon3b  37471  cmt2N  37517  cmt3N  37518  cvrcon3b  37544  cvrcmp2  37551  cvlexchb2  37598  cvlatexchb2  37602  2llnmj  37828  4atlem3  37864  4atlem9  37871  4atlem10a  37872  4atlem11a  37875  4atlem12a  37878  4at2  37882  2lplnmj  37890  llnexchb2  38137  lautlt  38359  lautcvr  38360  lautco  38365  ltrnatb  38405  ltrneq2  38416  cdlemefrs29pre00  38663  cdlemefrs29cpre1  38666  cdleme32fva  38705  dibglbN  39434  dochsncom  39650  dochkrsat  39723  lspindp5  40038  mapdh8ab  40045  hdmapip0com  40185  fsuppind  40539  dvdsexpb  40602  sn-ltmul2d  40691  prjsprellsp  40710  lzenom  40854  rmxycomplete  41002  fzneg  41067  modabsdifz  41071  jm2.19  41078  pw2f1ocnv  41122  fzunt  41384  fzuntd  41385  fzunt1d  41386  fzuntgd  41387  sqrtcvallem1  41560  brtrclfv2  41656  rfovcnvf1od  41933  ntrclsfveq1  41991  ntrclsiso  41998  k0004lem2  42079  caofcan  42262  rfcnpre1  42883  rfcnpre2  42895  ellimcabssub0  43494  liminfpnfuz  43693  xlimpnfxnegmnf2  43735  fperdvper  43796  vonvolmbl  44536  readdcnnred  45146  resubcnnred  45147  cndivrenred  45149  requad2  45426  mgmpropd  45680  lco0  46119  lindslininds  46156  ltsubaddb  46206  ltsubsubb  46207  ltsubadd2b  46208  elbigolo1  46254  dig2bits  46311  rrx2pnedifcoorneorr  46414  mofeu  46526  sepnsepo  46568  lubeldm2d  46603  glbeldm2d  46604  thincsect2  46690  thinccic  46693  postcposALT  46713