Theorem 3bitr4d 312

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sbccomlem  3808  pr1eqbg  4795  unisucg  6397  fimarab  6908  fvopab3g  6937  fvimacnvALT  7005  respreima  7014  fmptco  7078  fnnfpeq0  7129  cocan1  7242  cocan2  7243  caofidlcan  7665  ordsucelsuc  7769  ordsucsssuc  7770  fnsuppres  8138  smoword  8303  oaword  8481  omword  8502  om00el  8508  oeword  8523  nnaword  8560  nnmword  8566  eldifsucnn  8597  naddss1  8622  naddunif  8626  swoer  8672  erth  8695  brecop  8754  eceqoveq  8766  xpdom2  9007  pw2f1olem  9016  ixpfi2  9257  cantnfrescl  9595  ttrclselem2  9645  rankr1bg  9725  r1pwcl  9769  fseqenlem1  9944  alephord3  9998  alephdom2  10007  engch  10549  fpwwe2lem6  10557  fpwwe2lem8  10559  ltexpi  10823  ltapi  10824  ltmpi  10825  ltsonq  10890  ltmnq  10893  1idpr  10950  addcanpr  10967  axpre-ltadd  11088  axlttri  11215  subsub23  11396  leadd1  11616  ltsub1  11644  ltsub2  11645  leord1  11675  eqord1  11676  lemul1  12005  lediv1  12019  lt2mul2div  12032  lerec  12037  lediv2  12044  le2msq  12054  suprleub  12120  infregelb  12138  ofsubeq0  12154  ofsubge0  12156  indpi1  12171  avgle1  12415  avgle2  12416  cnref1o  12933  xleneg  13168  xnn0lem1lt  13194  xltadd1  13206  xsubge0  13211  xposdif  13212  xltmul1  13242  supxrleub  13276  infxrgelb  13286  iooneg  13422  iccneg  13423  iccsplit  13436  iccshftr  13437  iccshftl  13439  iccdil  13441  icccntr  13443  fzsplit2  13501  fzaddel  13510  fzrev  13539  predfz  13605  elfzo  13613  nelfzo  13617  fzon  13633  elfzom1b  13719  negmod0  13835  leexp2  14131  ltexp2r  14133  repswsymball  14739  repswsymballbi  14740  cjreb  15083  sqrtlt  15221  limsuplt  15439  o1lo1  15497  rlimresb  15525  lo1eq  15528  rlimeq  15529  o1eq  15530  isercoll  15628  efle  16083  tanaddlem  16131  nndivdvds  16228  moddvds  16230  modmulconst  16255  oddm1even  16310  ltoddhalfle  16328  bitsp1  16398  sadcaddlem  16424  sadadd  16434  sadass  16438  bitsshft  16442  smuval2  16449  smumul  16460  dvdssq  16534  phiprmpw  16744  eulerthlem2  16750  odzdvds  16764  pc2dvds  16848  1arith  16896  imasleval  17503  mreacs  17622  catpropd  17673  oppcsect  17743  funcres2b  17862  fthsect  17892  fthinv  17893  fucsect  17940  fucinv  17941  latnlemlt  18436  latnle  18437  ipole  18498  ipolt  18499  mgmpropd  18617  issubg3  19118  eqgid  19153  resghm2b  19207  conjghm  19222  ghmqusker  19260  gastacos  19283  resscntz  19306  cntzrec  19309  oppgsubm  19335  oppgsubg  19336  sylow3lem6  19605  lsmcom2  19628  lsmass  19642  ablsubsub23  19797  lsmcomx  19829  subgdmdprd  20009  opprsubrng  20538  opprsubrg  20572  lsslss  20958  lbspropd  21096  islbs2  21154  rspsn  21333  prmirred  21456  znfld  21542  lindfmm  21809  lindsmm  21810  lsslindf  21812  lsslinds  21813  islindf4  21820  psrbagconf1o  21911  gsumbagdiaglem  21913  mplmonmul  22019  basdif0  22943  neiptopreu  23123  neitr  23170  restlp  23173  cnrest2  23276  cnprest  23279  cnprest2  23280  lmss  23288  lmff  23291  ist1-2  23337  lpcls  23354  perfcls  23355  cmpfi  23398  hauseqlcld  23636  txlm  23638  txkgen  23642  xkopt  23645  idqtop  23696  tgqtop  23702  qtopcn  23704  uffix  23911  fmco  23951  flimrest  23973  lmflf  23995  txflf  23996  fclsrest  24014  cnpfcf  24031  tsmsgsum  24129  tsmsres  24134  tsmsf1o  24135  fmucndlem  24280  ismet2  24323  imasf1oxmet  24365  blres  24421  xmetec  24424  imasf1obl  24478  imasf1oxms  24479  prdsbl  24481  stdbdbl  24507  metrest  24514  metustsym  24545  blval2  24552  metuel2  24555  tngngp  24644  cnbl0  24763  cnblcld  24764  bl2ioo  24782  cncfcnvcn  24917  iihalf2  24925  icoopnst  24931  iocopnst  24932  icopnfcnv  24934  icopnfhmeo  24935  cphorthcom  25193  caucfil  25275  lmclim  25295  cmsss  25343  rrxmet  25400  volsup  25548  dyaddisjlem  25587  mbfeqalem1  25633  mbfeqalem2  25634  mbfeqa  25635  mbfmulc2lem  25639  mbfmax  25641  mbfposr  25644  ismbf3d  25646  mbfimaopnlem  25647  mbfaddlem  25652  mbfsup  25656  mbfinf  25657  0plef  25664  0pledm  25665  i1fmulclem  25694  i1fres  25697  i1fpos  25698  itg1climres  25706  mbfi1fseqlem4  25710  itg2mulclem  25738  itg2monolem1  25742  itg2cnlem1  25753  iblre  25786  iblcn  25791  itgeqa  25806  ellimc2  25869  limcflf  25873  dvreslem  25901  lhop1  26006  r1pid2  26152  ply1remlem  26155  fta1glem2  26159  ofmulrt  26273  plydiveu  26289  plyremlem  26295  quotcan  26300  ulmres  26378  cos11  26522  logleb  26592  argrege0  26600  logdivle  26611  efopn  26647  logccv  26652  cxplt  26683  cxple  26684  cxple2  26686  cxplt2  26687  cxplt3  26689  cxple3  26690  recxpf1lem  26718  logbleb  26772  logblt  26773  angrtmuld  26797  quad2  26828  atans2  26920  rlimcnp  26954  rlimcnp2  26955  rlimcxp  26962  sqff1o  27170  fsumvma2  27202  dchrptlem2  27253  lgsdilem  27312  lgsne0  27323  lgsqr  27339  lgsquadlem1  27368  lgsquadlem2  27369  m1lgs  27376  2lgslem1a  27379  2lgs  27395  dchrisum0lem1  27504  padicabv  27618  nosupinfsep  27721  oldlim  27904  newbday  27919  leslss  27926  ltadds2  28008  lenegs  28063  ltsubs2  28094  ltsubsubsbd  28100  lesubsubsbd  28103  lesubsubs2bd  28104  lesubsubs3bd  28105  lesubsd  28113  lemuls2d  28191  lemuls1d  28192  ltmulnegs1d  28193  onles  28285  n0subs2  28381  bdaypw2bnd  28482  bdayfinbndlem1  28484  trgcgrg  28608  colcom  28651  colrot1  28652  ishlg  28695  hlcomb  28696  hlbtwn  28704  lncom  28715  lnrot2  28717  israg  28790  perpcom  28806  hpgcom  28860  colopp  28862  iscgra  28902  isinag  28931  colinearalglem2  29001  axcgrid  29010  uvtx01vtx  29491  iscplgredg  29511  rgrusgrprc  29683  uspgr2wlkeq  29739  dfpth2  29822  clwlkclwwlk  30097  eupth2lem3lem6  30328  fusgr2wsp2nb  30429  nmorepnf  30864  blocnilem  30900  ubthlem1  30966  shscom  31415  pjpreeq  31494  spansncol  31664  cmcm2  31712  hodsi  31871  nmoprepnf  31963  nmfnrepnf  31976  pjssposi  32268  cvcon3  32380  mdsymlem8  32506  dmdsym  32509  disjunsn  32690  unipreima  32742  fmptcof2  32756  fdifsupp  32784  ressupprn  32789  1stpreima  32806  fpwrelmapffslem  32831  infxrge0gelb  32865  nndiffz1  32885  prodindf  32948  indf1ofs  32952  mgccnv  33085  pwrssmgc  33086  gsumwrd2dccatlem  33165  cntzun  33167  cntrval2  33259  isinftm  33269  domnprodeq0  33364  qusxpid  33453  lindfpropd  33472  lindspropd  33473  unitprodclb  33479  lsmssass  33492  nsgmgc  33502  crngmxidl  33559  opprqusdrng  33583  qsfld  33588  ply1dg1rt  33670  selvply1rhmlemb  33710  psrmonmul  33741  finexttrb  33856  algextdeglem7  33914  ist0cld  34024  metidv  34083  metider  34085  pstmxmet  34088  xrge0iifiso  34126  aean  34435  brfae  34439  signsply0  34742  signsvfn  34773  reprinrn  34809  subfacp1lem3  35417  subfacp1lem5  35419  fmlafvel  35620  opelco3  36010  sscoid  36146  cgrcomr  36232  ofscom  36242  cgr3permute3  36282  cgr3permute1  36283  cgr3com  36288  colinearperm1  36297  colinearperm3  36298  outsideofcom  36363  opnbnd  36560  filnetlem4  36616  finxpsuclem  37766  wl-equsald  37917  wl-equsaldv  37918  lindsadd  37987  poimirlem23  38017  broucube  38028  heicant  38029  itg2addnclem2  38046  ftc1anclem1  38067  ftc1anclem5  38071  ftc1anclem6  38072  areacirclem5  38086  areacirc  38087  caures  38134  cnpwstotbnd  38171  ismtyima  38177  rrnmet  38203  reheibor  38213  rngosn3  38298  ecxrn2  38782  brcosscnvcoss  38898  br1cosscnvxrn  38938  eqvrelth  39069  brpartspart  39250  lcvbr  39520  lkrsc  39596  lshpkrlem1  39609  opltcon3b  39703  cmt2N  39749  cmt3N  39750  cvrcon3b  39776  cvrcmp2  39783  cvlexchb2  39830  cvlatexchb2  39834  2llnmj  40059  4atlem3  40095  4atlem9  40102  4atlem10a  40103  4atlem11a  40106  4atlem12a  40109  4at2  40113  2lplnmj  40121  llnexchb2  40368  lautlt  40590  lautcvr  40591  lautco  40596  ltrnatb  40636  ltrneq2  40647  cdlemefrs29pre00  40894  cdlemefrs29cpre1  40897  cdleme32fva  40936  dibglbN  41665  dochsncom  41881  dochkrsat  41954  lspindp5  42269  mapdh8ab  42276  hdmapip0com  42416  dvdsexpb  42819  sn-ltmul2d  42970  fsuppind  43047  prjsprellsp  43068  lzenom  43226  rmxycomplete  43369  fzneg  43434  modabsdifz  43438  jm2.19  43445  pw2f1ocnv  43489  nadd1suc  43844  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  sqrtcvallem1  44082  brtrclfv2  44178  rfovcnvf1od  44455  ntrclsfveq1  44511  ntrclsiso  44518  k0004lem2  44599  caofcan  44774  rfcnpre1  45474  rfcnpre2  45486  ellimcabssub0  46069  liminfpnfuz  46266  xlimpnfxnegmnf2  46308  fperdvper  46369  vonvolmbl  47111  readdcnnred  47773  resubcnnred  47774  cndivrenred  47776  submodaddmod  47817  minusmodnep2tmod  47829  requad2  48121  uhgrimisgrgric  48429  clnbgrgrim  48432  lco0  48925  lindslininds  48962  ltsubaddb  49012  ltsubsubb  49013  ltsubadd2b  49014  elbigolo1  49055  dig2bits  49112  rrx2pnedifcoorneorr  49215  mofeu  49345  sepnsepo  49421  lubeldm2d  49455  glbeldm2d  49456  cicpropdlem  49546  uptra  49712  uptr2a  49719  thincsect2  49965  thinccic  49968  isinito2lem  49995  postcposALT  50065  lanup  50138  ranup  50139  lmddu  50164