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:  sbccomlem  3822  pr1eqbg  4814  unisucg  6422  fimarab  6937  fvopab3g  6966  fvimacnvALT  7034  respreima  7043  fmptco  7107  fnnfpeq0  7158  cocan1  7271  cocan2  7272  caofidlcan  7694  ordsucelsuc  7798  ordsucsssuc  7799  fnsuppres  8166  smoword  8332  oaword  8513  omword  8534  om00el  8540  oeword  8555  nnaword  8592  nnmword  8598  eldifsucnn  8629  naddss1  8655  naddunif  8659  swoer  8705  erth  8728  brecop  8787  eceqoveq  8799  xpdom2  9040  pw2f1olem  9049  ixpfi2  9290  cantnfrescl  9628  ttrclselem2  9678  rankr1bg  9758  r1pwcl  9802  fseqenlem1  9977  alephord3  10031  alephdom2  10040  engch  10583  fpwwe2lem6  10591  fpwwe2lem8  10593  ltexpi  10857  ltapi  10858  ltmpi  10859  ltsonq  10924  ltmnq  10927  1idpr  10984  addcanpr  11001  axpre-ltadd  11122  axlttri  11251  subsub23  11432  leadd1  11652  ltsub1  11680  ltsub2  11681  leord1  11711  eqord1  11712  lemul1  12040  lediv1  12054  lt2mul2div  12067  lerec  12072  lediv2  12079  le2msq  12089  suprleub  12155  infregelb  12173  ofsubeq0  12189  ofsubge0  12191  indpi1  12206  avgle1  12458  avgle2  12459  cnref1o  12983  xleneg  13218  xnn0lem1lt  13244  xltadd1  13256  xsubge0  13261  xposdif  13262  xltmul1  13292  supxrleub  13326  infxrgelb  13336  iooneg  13472  iccneg  13473  iccsplit  13486  iccshftr  13487  iccshftl  13489  iccdil  13491  icccntr  13493  fzsplit2  13551  fzaddel  13560  fzrev  13589  predfz  13655  elfzo  13663  nelfzo  13667  fzon  13683  elfzom1b  13769  negmod0  13885  leexp2  14181  ltexp2r  14183  repswsymball  14789  repswsymballbi  14790  cjreb  15133  sqrtlt  15271  limsuplt  15489  o1lo1  15547  rlimresb  15575  lo1eq  15578  rlimeq  15579  o1eq  15580  isercoll  15678  efle  16133  tanaddlem  16181  nndivdvds  16278  moddvds  16280  modmulconst  16305  oddm1even  16360  ltoddhalfle  16378  bitsp1  16448  sadcaddlem  16474  sadadd  16484  sadass  16488  bitsshft  16492  smuval2  16499  smumul  16510  dvdssq  16584  phiprmpw  16794  eulerthlem2  16800  odzdvds  16814  pc2dvds  16898  1arith  16946  imasleval  17554  mreacs  17673  catpropd  17724  oppcsect  17794  funcres2b  17913  fthsect  17943  fthinv  17944  fucsect  17991  fucinv  17992  latnlemlt  18487  latnle  18488  ipole  18549  ipolt  18550  mgmpropd  18668  issubg3  19169  eqgid  19204  resghm2b  19257  conjghm  19272  ghmqusker  19310  gastacos  19333  resscntz  19356  cntzrec  19359  oppgsubm  19385  oppgsubg  19386  sylow3lem6  19655  lsmcom2  19678  lsmass  19692  ablsubsub23  19847  lsmcomx  19879  subgdmdprd  20059  opprsubrng  20588  opprsubrg  20622  lsslss  21008  lbspropd  21146  islbs2  21204  rspsn  21383  prmirred  21506  znfld  21592  lindfmm  21859  lindsmm  21860  lsslindf  21862  lsslinds  21863  islindf4  21870  psrbagconf1o  21961  gsumbagdiaglem  21963  mplmonmul  22069  basdif0  22993  neiptopreu  23173  neitr  23220  restlp  23223  cnrest2  23326  cnprest  23329  cnprest2  23330  lmss  23338  lmff  23341  ist1-2  23387  lpcls  23404  perfcls  23405  cmpfi  23448  hauseqlcld  23686  txlm  23688  txkgen  23692  xkopt  23695  idqtop  23746  tgqtop  23752  qtopcn  23754  uffix  23961  fmco  24001  flimrest  24023  lmflf  24045  txflf  24046  fclsrest  24064  cnpfcf  24081  tsmsgsum  24179  tsmsres  24184  tsmsf1o  24185  fmucndlem  24330  ismet2  24373  imasf1oxmet  24415  blres  24471  xmetec  24474  imasf1obl  24528  imasf1oxms  24529  prdsbl  24531  stdbdbl  24557  metrest  24564  metustsym  24595  blval2  24602  metuel2  24605  tngngp  24694  cnbl0  24813  cnblcld  24814  bl2ioo  24832  cncfcnvcn  24967  iihalf2  24975  icoopnst  24981  iocopnst  24982  icopnfcnv  24984  icopnfhmeo  24985  cphorthcom  25243  caucfil  25325  lmclim  25345  cmsss  25393  rrxmet  25450  volsup  25598  dyaddisjlem  25637  mbfeqalem1  25683  mbfeqalem2  25684  mbfeqa  25685  mbfmulc2lem  25689  mbfmax  25691  mbfposr  25694  ismbf3d  25696  mbfimaopnlem  25697  mbfaddlem  25702  mbfsup  25706  mbfinf  25707  0plef  25714  0pledm  25715  i1fmulclem  25744  i1fres  25747  i1fpos  25748  itg1climres  25756  mbfi1fseqlem4  25760  itg2mulclem  25788  itg2monolem1  25792  itg2cnlem1  25803  iblre  25836  iblcn  25841  itgeqa  25856  ellimc2  25919  limcflf  25923  dvreslem  25951  lhop1  26056  r1pid2  26202  ply1remlem  26205  fta1glem2  26209  ofmulrt  26323  plydiveu  26339  plyremlem  26345  quotcan  26350  ulmres  26428  cos11  26575  logleb  26645  argrege0  26653  logdivle  26664  efopn  26700  logccv  26705  cxplt  26736  cxple  26737  cxple2  26739  cxplt2  26740  cxplt3  26742  cxple3  26743  recxpf1lem  26771  logbleb  26825  logblt  26826  angrtmuld  26850  quad2  26881  atans2  26973  rlimcnp  27007  rlimcnp2  27008  rlimcxp  27015  sqff1o  27223  fsumvma2  27255  dchrptlem2  27306  lgsdilem  27365  lgsne0  27376  lgsqr  27392  lgsquadlem1  27421  lgsquadlem2  27422  m1lgs  27429  2lgslem1a  27432  2lgs  27448  dchrisum0lem1  27557  padicabv  27671  nosupinfsep  27773  oldlim  27957  newbday  27972  leslss  27979  ltadds2  28061  lenegs  28116  ltsubs2  28147  ltsubsubsbd  28153  lesubsubsbd  28156  lesubsubs2bd  28157  lesubsubs3bd  28158  lesubsd  28166  lemuls2d  28244  lemuls1d  28245  ltmulnegs1d  28246  onles  28338  n0subs2  28434  bdaypw2bnd  28535  bdayfinbndlem1  28537  trgcgrg  28661  colcom  28704  colrot1  28705  ishlg  28748  hlcomb  28749  hlbtwn  28757  lncom  28768  lnrot2  28770  israg  28843  perpcom  28859  hpgcom  28913  colopp  28915  iscgra  28955  isinag  28984  colinearalglem2  29054  axcgrid  29063  uvtx01vtx  29544  iscplgredg  29564  rgrusgrprc  29736  uspgr2wlkeq  29792  dfpth2  29875  clwlkclwwlk  30150  eupth2lem3lem6  30381  fusgr2wsp2nb  30482  nmorepnf  30917  blocnilem  30953  ubthlem1  31019  shscom  31468  pjpreeq  31547  spansncol  31717  cmcm2  31765  hodsi  31924  nmoprepnf  32016  nmfnrepnf  32029  pjssposi  32321  cvcon3  32433  mdsymlem8  32559  dmdsym  32562  disjunsn  32743  unipreima  32795  fmptcof2  32809  fdifsupp  32837  ressupprn  32842  1stpreima  32859  fpwrelmapffslem  32884  infxrge0gelb  32918  nndiffz1  32938  prodindf  33001  indf1ofs  33005  mgccnv  33138  pwrssmgc  33139  gsumwrd2dccatlem  33218  cntzun  33220  cntrval2  33312  isinftm  33322  domnprodeq0  33421  qusxpid  33510  lindfpropd  33529  lindspropd  33530  unitprodclb  33536  lsmssass  33549  nsgmgc  33559  crngmxidl  33618  opprqusdrng  33642  qsfld  33647  ply1dg1rt  33737  selvply1rhmlemb  33777  psrmonmul  33808  finexttrb  33923  algextdeglem7  33981  ist0cld  34091  metidv  34150  metider  34152  pstmxmet  34155  xrge0iifiso  34193  aean  34502  brfae  34506  signsply0  34809  signsvfn  34840  reprinrn  34876  subfacp1lem3  35496  subfacp1lem5  35498  fmlafvel  35699  opelco3  36089  sscoid  36225  cgrcomr  36311  ofscom  36321  cgr3permute3  36361  cgr3permute1  36362  cgr3com  36367  colinearperm1  36376  colinearperm3  36377  outsideofcom  36442  opnbnd  36649  filnetlem4  36705  finxpsuclem  37855  wl-equsald  38006  wl-equsaldv  38007  lindsadd  38076  poimirlem23  38106  broucube  38117  heicant  38118  itg2addnclem2  38135  ftc1anclem1  38156  ftc1anclem5  38160  ftc1anclem6  38161  areacirclem5  38175  areacirc  38176  caures  38223  cnpwstotbnd  38260  ismtyima  38266  rrnmet  38292  reheibor  38302  rngosn3  38387  ecxrn2  38871  brcosscnvcoss  38987  br1cosscnvxrn  39027  eqvrelth  39158  brpartspart  39339  lcvbr  39609  lkrsc  39685  lshpkrlem1  39698  opltcon3b  39792  cmt2N  39838  cmt3N  39839  cvrcon3b  39865  cvrcmp2  39872  cvlexchb2  39919  cvlatexchb2  39923  2llnmj  40148  4atlem3  40184  4atlem9  40191  4atlem10a  40192  4atlem11a  40195  4atlem12a  40198  4at2  40202  2lplnmj  40210  llnexchb2  40457  lautlt  40679  lautcvr  40680  lautco  40685  ltrnatb  40725  ltrneq2  40736  cdlemefrs29pre00  40983  cdlemefrs29cpre1  40986  cdleme32fva  41025  dibglbN  41754  dochsncom  41970  dochkrsat  42043  lspindp5  42358  mapdh8ab  42365  hdmapip0com  42505  dvdsexpb  42908  sn-ltmul2d  43059  fsuppind  43136  prjsprellsp  43157  lzenom  43315  rmxycomplete  43458  fzneg  43523  modabsdifz  43527  jm2.19  43534  pw2f1ocnv  43578  nadd1suc  43933  fzunt  43995  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  sqrtcvallem1  44171  brtrclfv2  44267  rfovcnvf1od  44544  ntrclsfveq1  44600  ntrclsiso  44607  k0004lem2  44688  caofcan  44863  rfcnpre1  45563  rfcnpre2  45575  ellimcabssub0  46157  liminfpnfuz  46354  xlimpnfxnegmnf2  46396  fperdvper  46457  vonvolmbl  47199  readdcnnred  47861  resubcnnred  47862  cndivrenred  47864  submodaddmod  47905  minusmodnep2tmod  47917  requad2  48209  uhgrimisgrgric  48517  clnbgrgrim  48520  lco0  49013  lindslininds  49050  ltsubaddb  49100  ltsubsubb  49101  ltsubadd2b  49102  elbigolo1  49143  dig2bits  49200  rrx2pnedifcoorneorr  49303  mofeu  49433  sepnsepo  49509  lubeldm2d  49543  glbeldm2d  49544  cicpropdlem  49634  uptra  49800  uptr2a  49807  thincsect2  50053  thinccic  50056  isinito2lem  50083  postcposALT  50153  lanup  50226  ranup  50227  lmddu  50252