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 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  4788  fvopab3g  6879  fvimacnvALT  6943  respreima  6952  fmptco  7010  fnnfpeq0  7059  cocan1  7172  cocan2  7173  ordsucelsuc  7678  ordsucsssuc  7679  fnsuppres  8016  smoword  8206  oaword  8389  omword  8410  om00el  8416  oeword  8430  nnaword  8467  nnmword  8473  eldifsucnn  8503  swoer  8537  erth  8556  brecop  8608  eceqoveq  8620  xpdom2  8863  pw2f1olem  8872  ixpfi2  9126  cantnfrescl  9443  ttrclselem2  9493  rankr1bg  9570  r1pwcl  9614  fseqenlem1  9789  alephord3  9843  alephdom2  9852  engch  10393  fpwwe2lem6  10401  fpwwe2lem8  10403  ltexpi  10667  ltapi  10668  ltmpi  10669  ltsonq  10734  ltmnq  10737  1idpr  10794  addcanpr  10811  axpre-ltadd  10932  axlttri  11055  subsub23  11235  leadd1  11452  ltsub1  11480  ltsub2  11481  leord1  11511  eqord1  11512  lemul1  11836  lediv1  11849  lt2mul2div  11862  lerec  11867  lediv2  11874  le2msq  11884  suprleub  11950  infregelb  11968  ofsubeq0  11979  ofsubge0  11981  avgle1  12222  avgle2  12223  cnref1o  12734  xleneg  12961  xnn0lem1lt  12987  xltadd1  12999  xsubge0  13004  xposdif  13005  xltmul1  13035  supxrleub  13069  infxrgelb  13078  iooneg  13212  iccneg  13213  iccsplit  13226  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  fzsplit2  13290  fzaddel  13299  fzrev  13328  predfz  13390  elfzo  13398  nelfzo  13401  fzon  13417  elfzom1b  13495  negmod0  13607  leexp2  13898  ltexp2r  13900  repswsymball  14501  repswsymballbi  14502  cjreb  14843  sqrtlt  14982  limsuplt  15197  o1lo1  15255  rlimresb  15283  lo1eq  15286  rlimeq  15287  o1eq  15288  isercoll  15388  efle  15836  tanaddlem  15884  nndivdvds  15981  moddvds  15983  modmulconst  16006  oddm1even  16061  ltoddhalfle  16079  bitsp1  16147  sadcaddlem  16173  sadadd  16183  sadass  16187  bitsshft  16191  smuval2  16198  smumul  16209  dvdssq  16281  phiprmpw  16486  eulerthlem2  16492  odzdvds  16505  pc2dvds  16589  1arith  16637  imasleval  17261  mreacs  17376  catpropd  17427  oppcsect  17499  funcres2b  17621  fthsect  17650  fthinv  17651  fucsect  17699  fucinv  17700  latnlemlt  18199  latnle  18200  ipole  18261  ipolt  18262  issubg3  18782  eqgid  18817  resghm2b  18861  conjghm  18874  gastacos  18925  resscntz  18947  cntzrec  18949  oppgsubm  18978  oppgsubg  18979  sylow3lem6  19246  lsmcom2  19269  lsmass  19284  ablsubsub23  19435  lsmcomx  19466  subgdmdprd  19646  opprsubrg  20054  lsslss  20232  lbspropd  20370  islbs2  20425  rspsn  20534  prmirred  20705  znfld  20777  lindfmm  21043  lindsmm  21044  lsslindf  21046  lsslinds  21047  islindf4  21054  psrbagconf1o  21148  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  mplmonmul  21246  basdif0  22112  neiptopreu  22293  neitr  22340  restlp  22343  cnrest2  22446  cnprest  22449  cnprest2  22450  lmss  22458  lmff  22461  ist1-2  22507  lpcls  22524  perfcls  22525  cmpfi  22568  hauseqlcld  22806  txlm  22808  txkgen  22812  xkopt  22815  idqtop  22866  tgqtop  22872  qtopcn  22874  uffix  23081  fmco  23121  flimrest  23143  lmflf  23165  txflf  23166  fclsrest  23184  cnpfcf  23201  tsmsgsum  23299  tsmsres  23304  tsmsf1o  23305  fmucndlem  23452  ismet2  23495  imasf1oxmet  23537  blres  23593  xmetec  23596  imasf1obl  23653  imasf1oxms  23654  prdsbl  23656  stdbdbl  23682  metrest  23689  metustsym  23720  blval2  23727  metuel2  23730  tngngp  23827  cnbl0  23946  cnblcld  23947  bl2ioo  23964  cncfcnvcn  24097  iihalf2  24105  icoopnst  24111  iocopnst  24112  icopnfcnv  24114  icopnfhmeo  24115  cphorthcom  24374  caucfil  24456  lmclim  24476  cmsss  24524  rrxmet  24581  volsup  24729  dyaddisjlem  24768  mbfeqalem1  24814  mbfeqalem2  24815  mbfeqa  24816  mbfmulc2lem  24820  mbfmax  24822  mbfposr  24825  ismbf3d  24827  mbfimaopnlem  24828  mbfaddlem  24833  mbfsup  24837  mbfinf  24838  0plef  24845  0pledm  24846  i1fmulclem  24876  i1fres  24879  i1fpos  24880  itg1climres  24888  mbfi1fseqlem4  24892  itg2mulclem  24920  itg2monolem1  24924  itg2cnlem1  24935  iblre  24967  iblcn  24972  itgeqa  24987  ellimc2  25050  limcflf  25054  dvreslem  25082  lhop1  25187  ply1remlem  25336  fta1glem2  25340  ofmulrt  25451  plydiveu  25467  plyremlem  25473  quotcan  25478  ulmres  25556  cos11  25698  logleb  25767  argrege0  25775  logdivle  25786  efopn  25822  logccv  25827  cxplt  25858  cxple  25859  cxple2  25861  cxplt2  25862  cxplt3  25864  cxple3  25865  logbleb  25942  logblt  25943  angrtmuld  25967  quad2  25998  atans2  26090  rlimcnp  26124  rlimcnp2  26125  rlimcxp  26132  sqff1o  26340  fsumvma2  26371  dchrptlem2  26422  lgsdilem  26481  lgsne0  26492  lgsqr  26508  lgsquadlem1  26537  lgsquadlem2  26538  m1lgs  26545  2lgslem1a  26548  2lgs  26564  dchrisum0lem1  26673  padicabv  26787  trgcgrg  26885  colcom  26928  colrot1  26929  ishlg  26972  hlcomb  26973  hlbtwn  26981  lncom  26992  lnrot2  26994  israg  27067  perpcom  27083  hpgcom  27137  colopp  27139  iscgra  27179  isinag  27208  colinearalglem2  27284  axcgrid  27293  uvtx01vtx  27773  iscplgredg  27793  rgrusgrprc  27965  uspgr2wlkeq  28022  clwlkclwwlk  28375  eupth2lem3lem6  28606  fusgr2wsp2nb  28707  nmorepnf  29139  blocnilem  29175  ubthlem1  29241  shscom  29690  pjpreeq  29769  spansncol  29939  cmcm2  29987  hodsi  30146  nmoprepnf  30238  nmfnrepnf  30251  pjssposi  30543  cvcon3  30655  mdsymlem8  30781  dmdsym  30784  disjunsn  30942  fimarab  30989  unipreima  30990  fmptcof2  31003  ressupprn  31033  1stpreima  31048  fpwrelmapffslem  31076  infxrge0gelb  31098  nndiffz1  31116  mgccnv  31286  pwrssmgc  31287  cntzun  31329  isinftm  31444  qusxpid  31568  lindfpropd  31585  lindspropd  31586  lsmssass  31599  nsgmgc  31606  finexttrb  31746  ist0cld  31792  metidv  31851  metider  31853  pstmxmet  31856  xrge0iifiso  31894  indpi1  31997  prodindf  32000  indf1ofs  32003  aean  32221  brfae  32225  signsply0  32539  signsvfn  32570  reprinrn  32607  subfacp1lem3  33153  subfacp1lem5  33155  fmlafvel  33356  opelco3  33758  naddss1  33850  nosupinfsep  33944  oldlim  34078  newbday  34091  sscoid  34224  cgrcomr  34308  ofscom  34318  cgr3permute3  34358  cgr3permute1  34359  cgr3com  34364  colinearperm1  34373  colinearperm3  34374  outsideofcom  34439  opnbnd  34523  filnetlem4  34579  finxpsuclem  35577  wl-equsald  35707  lindsadd  35779  poimirlem23  35809  broucube  35820  heicant  35821  itg2addnclem2  35838  ftc1anclem1  35859  ftc1anclem5  35863  ftc1anclem6  35864  areacirclem5  35878  areacirc  35879  caures  35927  cnpwstotbnd  35964  ismtyima  35970  rrnmet  35996  reheibor  36006  rngosn3  36091  brcosscnvcoss  36564  br1cosscnvxrn  36599  eqvrelth  36731  lcvbr  37042  lkrsc  37118  lshpkrlem1  37131  opltcon3b  37225  cmt2N  37271  cmt3N  37272  cvrcon3b  37298  cvrcmp2  37305  cvlexchb2  37352  cvlatexchb2  37356  2llnmj  37581  4atlem3  37617  4atlem9  37624  4atlem10a  37625  4atlem11a  37628  4atlem12a  37631  4at2  37635  2lplnmj  37643  llnexchb2  37890  lautlt  38112  lautcvr  38113  lautco  38118  ltrnatb  38158  ltrneq2  38169  cdlemefrs29pre00  38416  cdlemefrs29cpre1  38419  cdleme32fva  38458  dibglbN  39187  dochsncom  39403  dochkrsat  39476  lspindp5  39791  mapdh8ab  39798  hdmapip0com  39938  fsuppind  40286  dvdsexpb  40349  sn-ltmul2d  40438  prjsprellsp  40457  lzenom  40599  rmxycomplete  40746  fzneg  40811  modabsdifz  40815  jm2.19  40822  pw2f1ocnv  40866  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  sqrtcvallem1  41246  brtrclfv2  41342  rfovcnvf1od  41619  ntrclsfveq1  41677  ntrclsiso  41684  k0004lem2  41765  caofcan  41948  rfcnpre1  42569  rfcnpre2  42581  ellimcabssub0  43165  liminfpnfuz  43364  xlimpnfxnegmnf2  43406  fperdvper  43467  vonvolmbl  44206  readdcnnred  44806  resubcnnred  44807  cndivrenred  44809  requad2  45086  mgmpropd  45340  lco0  45779  lindslininds  45816  ltsubaddb  45866  ltsubsubb  45867  ltsubadd2b  45868  elbigolo1  45914  dig2bits  45971  rrx2pnedifcoorneorr  46074  mofeu  46186  sepnsepo  46228  lubeldm2d  46263  glbeldm2d  46264  thincsect2  46350  thinccic  46353  postcposALT  46373