Theorem 3bitr4d 311

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbccomlem  3844  pr1eqbg  4833  unisucg  6431  fimarab  6952  fvopab3g  6980  fvimacnvALT  7046  respreima  7055  fmptco  7118  fnnfpeq0  7169  cocan1  7283  cocan2  7284  caofidlcan  7707  ordsucelsuc  7814  ordsucsssuc  7815  fnsuppres  8188  smoword  8378  oaword  8559  omword  8580  om00el  8586  oeword  8600  nnaword  8637  nnmword  8643  eldifsucnn  8674  naddss1  8699  naddunif  8703  swoer  8748  erth  8768  brecop  8822  eceqoveq  8834  xpdom2  9079  pw2f1olem  9088  ixpfi2  9360  cantnfrescl  9688  ttrclselem2  9738  rankr1bg  9815  r1pwcl  9859  fseqenlem1  10036  alephord3  10090  alephdom2  10099  engch  10640  fpwwe2lem6  10648  fpwwe2lem8  10650  ltexpi  10914  ltapi  10915  ltmpi  10916  ltsonq  10981  ltmnq  10984  1idpr  11041  addcanpr  11058  axpre-ltadd  11179  axlttri  11304  subsub23  11485  leadd1  11703  ltsub1  11731  ltsub2  11732  leord1  11762  eqord1  11763  lemul1  12091  lediv1  12105  lt2mul2div  12118  lerec  12123  lediv2  12130  le2msq  12140  suprleub  12206  infregelb  12224  ofsubeq0  12235  ofsubge0  12237  avgle1  12479  avgle2  12480  cnref1o  12999  xleneg  13232  xnn0lem1lt  13258  xltadd1  13270  xsubge0  13275  xposdif  13276  xltmul1  13306  supxrleub  13340  infxrgelb  13350  iooneg  13486  iccneg  13487  iccsplit  13500  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  fzsplit2  13564  fzaddel  13573  fzrev  13602  predfz  13668  elfzo  13676  nelfzo  13679  fzon  13695  elfzom1b  13780  negmod0  13893  leexp2  14187  ltexp2r  14189  repswsymball  14795  repswsymballbi  14796  cjreb  15140  sqrtlt  15278  limsuplt  15493  o1lo1  15551  rlimresb  15579  lo1eq  15582  rlimeq  15583  o1eq  15584  isercoll  15682  efle  16134  tanaddlem  16182  nndivdvds  16279  moddvds  16281  modmulconst  16305  oddm1even  16360  ltoddhalfle  16378  bitsp1  16448  sadcaddlem  16474  sadadd  16484  sadass  16488  bitsshft  16492  smuval2  16499  smumul  16510  dvdssq  16584  phiprmpw  16793  eulerthlem2  16799  odzdvds  16813  pc2dvds  16897  1arith  16945  imasleval  17553  mreacs  17668  catpropd  17719  oppcsect  17789  funcres2b  17908  fthsect  17938  fthinv  17939  fucsect  17986  fucinv  17987  latnlemlt  18480  latnle  18481  ipole  18542  ipolt  18543  mgmpropd  18627  issubg3  19125  eqgid  19161  resghm2b  19215  conjghm  19230  ghmqusker  19268  gastacos  19291  resscntz  19314  cntzrec  19317  oppgsubm  19343  oppgsubg  19344  sylow3lem6  19611  lsmcom2  19634  lsmass  19648  ablsubsub23  19803  lsmcomx  19835  subgdmdprd  20015  opprsubrng  20517  opprsubrg  20551  lsslss  20916  lbspropd  21055  islbs2  21113  rspsn  21292  prmirred  21433  znfld  21519  lindfmm  21785  lindsmm  21786  lsslindf  21788  lsslinds  21789  islindf4  21796  psrbagconf1o  21887  gsumbagdiaglem  21888  mplmonmul  21992  basdif0  22889  neiptopreu  23069  neitr  23116  restlp  23119  cnrest2  23222  cnprest  23225  cnprest2  23226  lmss  23234  lmff  23237  ist1-2  23283  lpcls  23300  perfcls  23301  cmpfi  23344  hauseqlcld  23582  txlm  23584  txkgen  23588  xkopt  23591  idqtop  23642  tgqtop  23648  qtopcn  23650  uffix  23857  fmco  23897  flimrest  23919  lmflf  23941  txflf  23942  fclsrest  23960  cnpfcf  23977  tsmsgsum  24075  tsmsres  24080  tsmsf1o  24081  fmucndlem  24227  ismet2  24270  imasf1oxmet  24312  blres  24368  xmetec  24371  imasf1obl  24425  imasf1oxms  24426  prdsbl  24428  stdbdbl  24454  metrest  24461  metustsym  24492  blval2  24499  metuel2  24502  tngngp  24591  cnbl0  24710  cnblcld  24711  bl2ioo  24729  cncfcnvcn  24868  iihalf2  24877  icoopnst  24885  iocopnst  24886  icopnfcnv  24889  icopnfhmeo  24890  cphorthcom  25151  caucfil  25233  lmclim  25253  cmsss  25301  rrxmet  25358  volsup  25507  dyaddisjlem  25546  mbfeqalem1  25592  mbfeqalem2  25593  mbfeqa  25594  mbfmulc2lem  25598  mbfmax  25600  mbfposr  25603  ismbf3d  25605  mbfimaopnlem  25606  mbfaddlem  25611  mbfsup  25615  mbfinf  25616  0plef  25623  0pledm  25624  i1fmulclem  25653  i1fres  25656  i1fpos  25657  itg1climres  25665  mbfi1fseqlem4  25669  itg2mulclem  25697  itg2monolem1  25701  itg2cnlem1  25712  iblre  25745  iblcn  25750  itgeqa  25765  ellimc2  25828  limcflf  25832  dvreslem  25860  lhop1  25969  r1pid2  26117  ply1remlem  26120  fta1glem2  26124  ofmulrt  26239  plydiveu  26256  plyremlem  26262  quotcan  26267  ulmres  26347  cos11  26492  logleb  26562  argrege0  26570  logdivle  26581  efopn  26617  logccv  26622  cxplt  26653  cxple  26654  cxple2  26656  cxplt2  26657  cxplt3  26659  cxple3  26660  recxpf1lem  26688  logbleb  26743  logblt  26744  angrtmuld  26768  quad2  26799  atans2  26891  rlimcnp  26925  rlimcnp2  26926  rlimcxp  26934  sqff1o  27142  fsumvma2  27175  dchrptlem2  27226  lgsdilem  27285  lgsne0  27296  lgsqr  27312  lgsquadlem1  27341  lgsquadlem2  27342  m1lgs  27349  2lgslem1a  27352  2lgs  27368  dchrisum0lem1  27477  padicabv  27591  nosupinfsep  27694  oldlim  27842  newbday  27857  slelss  27863  sltadd2  27941  sleneg  27995  sltsub2  28024  sltsubsubbd  28030  slesubsubbd  28033  slesubsub2bd  28034  slesubsub3bd  28035  slemul2d  28117  slemul1d  28118  sltmulneg1d  28119  trgcgrg  28440  colcom  28483  colrot1  28484  ishlg  28527  hlcomb  28528  hlbtwn  28536  lncom  28547  lnrot2  28549  israg  28622  perpcom  28638  hpgcom  28692  colopp  28694  iscgra  28734  isinag  28763  colinearalglem2  28832  axcgrid  28841  uvtx01vtx  29322  iscplgredg  29342  rgrusgrprc  29515  uspgr2wlkeq  29572  dfpth2  29657  clwlkclwwlk  29929  eupth2lem3lem6  30160  fusgr2wsp2nb  30261  nmorepnf  30695  blocnilem  30731  ubthlem1  30797  shscom  31246  pjpreeq  31325  spansncol  31495  cmcm2  31543  hodsi  31702  nmoprepnf  31794  nmfnrepnf  31807  pjssposi  32099  cvcon3  32211  mdsymlem8  32337  dmdsym  32340  disjunsn  32521  unipreima  32567  fmptcof2  32581  fdifsupp  32608  ressupprn  32613  1stpreima  32630  fpwrelmapffslem  32655  infxrge0gelb  32689  nndiffz1  32709  indpi1  32783  prodindf  32786  indf1ofs  32789  mgccnv  32925  pwrssmgc  32926  gsumwrd2dccatlem  33006  cntzun  33008  isinftm  33125  qusxpid  33324  lindfpropd  33343  lindspropd  33344  unitprodclb  33350  lsmssass  33363  nsgmgc  33373  crngmxidl  33430  opprqusdrng  33454  qsfld  33459  ply1dg1rt  33538  finexttrb  33652  algextdeglem7  33703  ist0cld  33810  metidv  33869  metider  33871  pstmxmet  33874  xrge0iifiso  33912  aean  34221  brfae  34225  signsply0  34529  signsvfn  34560  reprinrn  34596  subfacp1lem3  35150  subfacp1lem5  35152  fmlafvel  35353  opelco3  35738  sscoid  35877  cgrcomr  35961  ofscom  35971  cgr3permute3  36011  cgr3permute1  36012  cgr3com  36017  colinearperm1  36026  colinearperm3  36027  outsideofcom  36092  opnbnd  36289  filnetlem4  36345  finxpsuclem  37361  wl-equsald  37503  wl-equsaldv  37504  lindsadd  37583  poimirlem23  37613  broucube  37624  heicant  37625  itg2addnclem2  37642  ftc1anclem1  37663  ftc1anclem5  37667  ftc1anclem6  37668  areacirclem5  37682  areacirc  37683  caures  37730  cnpwstotbnd  37767  ismtyima  37773  rrnmet  37799  reheibor  37809  rngosn3  37894  brcosscnvcoss  38398  br1cosscnvxrn  38438  eqvrelth  38575  brpartspart  38737  lcvbr  38985  lkrsc  39061  lshpkrlem1  39074  opltcon3b  39168  cmt2N  39214  cmt3N  39215  cvrcon3b  39241  cvrcmp2  39248  cvlexchb2  39295  cvlatexchb2  39299  2llnmj  39525  4atlem3  39561  4atlem9  39568  4atlem10a  39569  4atlem11a  39572  4atlem12a  39575  4at2  39579  2lplnmj  39587  llnexchb2  39834  lautlt  40056  lautcvr  40057  lautco  40062  ltrnatb  40102  ltrneq2  40113  cdlemefrs29pre00  40360  cdlemefrs29cpre1  40363  cdleme32fva  40402  dibglbN  41131  dochsncom  41347  dochkrsat  41420  lspindp5  41735  mapdh8ab  41742  hdmapip0com  41882  dvdsexpb  42331  sn-ltmul2d  42451  fsuppind  42560  prjsprellsp  42581  lzenom  42740  rmxycomplete  42888  fzneg  42953  modabsdifz  42957  jm2.19  42964  pw2f1ocnv  43008  nadd1suc  43363  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  sqrtcvallem1  43602  brtrclfv2  43698  rfovcnvf1od  43975  ntrclsfveq1  44031  ntrclsiso  44038  k0004lem2  44119  caofcan  44295  rfcnpre1  44991  rfcnpre2  45003  ellimcabssub0  45594  liminfpnfuz  45793  xlimpnfxnegmnf2  45835  fperdvper  45896  vonvolmbl  46638  readdcnnred  47280  resubcnnred  47281  cndivrenred  47283  submodaddmod  47318  minusmodnep2tmod  47330  requad2  47585  uhgrimisgrgric  47892  clnbgrgrim  47895  lco0  48351  lindslininds  48388  ltsubaddb  48438  ltsubsubb  48439  ltsubadd2b  48440  elbigolo1  48485  dig2bits  48542  rrx2pnedifcoorneorr  48645  mofeu  48774  sepnsepo  48846  lubeldm2d  48880  glbeldm2d  48881  cicpropdlem  48964  thincsect2  49302  thinccic  49305  isinito2lem  49331  postcposALT  49393  lanup  49463  ranup  49464