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  4862  unisucg  6453  fvopab3g  7003  fvimacnvALT  7069  respreima  7078  fmptco  7142  fnnfpeq0  7191  cocan1  7304  cocan2  7305  ordsucelsuc  7830  ordsucsssuc  7831  fnsuppres  8204  smoword  8395  oaword  8578  omword  8599  om00el  8605  oeword  8619  nnaword  8656  nnmword  8662  eldifsucnn  8693  naddss1  8718  naddunif  8722  swoer  8764  erth  8784  brecop  8838  eceqoveq  8850  xpdom2  9104  pw2f1olem  9113  ixpfi2  9390  cantnfrescl  9715  ttrclselem2  9765  rankr1bg  9842  r1pwcl  9886  fseqenlem1  10063  alephord3  10117  alephdom2  10126  engch  10667  fpwwe2lem6  10675  fpwwe2lem8  10677  ltexpi  10941  ltapi  10942  ltmpi  10943  ltsonq  11008  ltmnq  11011  1idpr  11068  addcanpr  11085  axpre-ltadd  11206  axlttri  11331  subsub23  11511  leadd1  11728  ltsub1  11756  ltsub2  11757  leord1  11787  eqord1  11788  lemul1  12113  lediv1  12126  lt2mul2div  12139  lerec  12144  lediv2  12151  le2msq  12161  suprleub  12227  infregelb  12245  ofsubeq0  12256  ofsubge0  12258  avgle1  12499  avgle2  12500  cnref1o  13016  xleneg  13246  xnn0lem1lt  13272  xltadd1  13284  xsubge0  13289  xposdif  13290  xltmul1  13320  supxrleub  13354  infxrgelb  13363  iooneg  13497  iccneg  13498  iccsplit  13511  iccshftr  13512  iccshftl  13514  iccdil  13516  icccntr  13518  fzsplit2  13575  fzaddel  13584  fzrev  13613  predfz  13675  elfzo  13683  nelfzo  13686  fzon  13702  elfzom1b  13781  negmod0  13893  leexp2  14185  ltexp2r  14187  repswsymball  14782  repswsymballbi  14783  cjreb  15123  sqrtlt  15261  limsuplt  15476  o1lo1  15534  rlimresb  15562  lo1eq  15565  rlimeq  15566  o1eq  15567  isercoll  15667  efle  16115  tanaddlem  16163  nndivdvds  16260  moddvds  16262  modmulconst  16285  oddm1even  16340  ltoddhalfle  16358  bitsp1  16426  sadcaddlem  16452  sadadd  16462  sadass  16466  bitsshft  16470  smuval2  16477  smumul  16488  dvdssq  16563  phiprmpw  16773  eulerthlem2  16779  odzdvds  16792  pc2dvds  16876  1arith  16924  imasleval  17551  mreacs  17666  catpropd  17717  oppcsect  17789  funcres2b  17911  fthsect  17942  fthinv  17943  fucsect  17992  fucinv  17993  latnlemlt  18492  latnle  18493  ipole  18554  ipolt  18555  mgmpropd  18639  issubg3  19133  eqgid  19169  resghm2b  19223  conjghm  19238  ghmqusker  19276  gastacos  19299  resscntz  19322  cntzrec  19325  oppgsubm  19354  oppgsubg  19355  sylow3lem6  19625  lsmcom2  19648  lsmass  19662  ablsubsub23  19817  lsmcomx  19849  subgdmdprd  20029  opprsubrng  20536  opprsubrg  20572  lsslss  20885  lbspropd  21024  islbs2  21082  rspsn  21269  prmirred  21456  znfld  21550  lindfmm  21817  lindsmm  21818  lsslindf  21820  lsslinds  21821  islindf4  21828  psrbagconf1o  21926  psrbagconf1oOLD  21927  gsumbagdiaglemOLD  21928  gsumbagdiaglem  21931  mplmonmul  22035  basdif0  22939  neiptopreu  23120  neitr  23167  restlp  23170  cnrest2  23273  cnprest  23276  cnprest2  23277  lmss  23285  lmff  23288  ist1-2  23334  lpcls  23351  perfcls  23352  cmpfi  23395  hauseqlcld  23633  txlm  23635  txkgen  23639  xkopt  23642  idqtop  23693  tgqtop  23699  qtopcn  23701  uffix  23908  fmco  23948  flimrest  23970  lmflf  23992  txflf  23993  fclsrest  24011  cnpfcf  24028  tsmsgsum  24126  tsmsres  24131  tsmsf1o  24132  fmucndlem  24279  ismet2  24322  imasf1oxmet  24364  blres  24420  xmetec  24423  imasf1obl  24480  imasf1oxms  24481  prdsbl  24483  stdbdbl  24509  metrest  24516  metustsym  24547  blval2  24554  metuel2  24557  tngngp  24654  cnbl0  24773  cnblcld  24774  bl2ioo  24791  cncfcnvcn  24929  iihalf2  24938  icoopnst  24946  iocopnst  24947  icopnfcnv  24950  icopnfhmeo  24951  cphorthcom  25212  caucfil  25294  lmclim  25314  cmsss  25362  rrxmet  25419  volsup  25568  dyaddisjlem  25607  mbfeqalem1  25653  mbfeqalem2  25654  mbfeqa  25655  mbfmulc2lem  25659  mbfmax  25661  mbfposr  25664  ismbf3d  25666  mbfimaopnlem  25667  mbfaddlem  25672  mbfsup  25676  mbfinf  25677  0plef  25684  0pledm  25685  i1fmulclem  25715  i1fres  25718  i1fpos  25719  itg1climres  25727  mbfi1fseqlem4  25731  itg2mulclem  25759  itg2monolem1  25763  itg2cnlem1  25774  iblre  25806  iblcn  25811  itgeqa  25826  ellimc2  25889  limcflf  25893  dvreslem  25921  lhop1  26030  r1pid2  26181  ply1remlem  26184  fta1glem2  26188  ofmulrt  26301  plydiveu  26318  plyremlem  26324  quotcan  26329  ulmres  26409  cos11  26552  logleb  26622  argrege0  26630  logdivle  26641  efopn  26677  logccv  26682  cxplt  26713  cxple  26714  cxple2  26716  cxplt2  26717  cxplt3  26719  cxple3  26720  recxpf1lem  26748  logbleb  26803  logblt  26804  angrtmuld  26828  quad2  26859  atans2  26951  rlimcnp  26985  rlimcnp2  26986  rlimcxp  26994  sqff1o  27202  fsumvma2  27235  dchrptlem2  27286  lgsdilem  27345  lgsne0  27356  lgsqr  27372  lgsquadlem1  27401  lgsquadlem2  27402  m1lgs  27409  2lgslem1a  27412  2lgs  27428  dchrisum0lem1  27537  padicabv  27651  nosupinfsep  27754  oldlim  27902  newbday  27917  slelss  27923  sltadd2  27997  sleneg  28047  sltsub2  28076  sltsubsubbd  28082  slesubsubbd  28085  slesubsub2bd  28086  slesubsub3bd  28087  slemul2d  28167  slemul1d  28168  sltmulneg1d  28169  trgcgrg  28434  colcom  28477  colrot1  28478  ishlg  28521  hlcomb  28522  hlbtwn  28530  lncom  28541  lnrot2  28543  israg  28616  perpcom  28632  hpgcom  28686  colopp  28688  iscgra  28728  isinag  28757  colinearalglem2  28833  axcgrid  28842  uvtx01vtx  29325  iscplgredg  29345  rgrusgrprc  29518  uspgr2wlkeq  29575  clwlkclwwlk  29927  eupth2lem3lem6  30158  fusgr2wsp2nb  30259  nmorepnf  30693  blocnilem  30729  ubthlem1  30795  shscom  31244  pjpreeq  31323  spansncol  31493  cmcm2  31541  hodsi  31700  nmoprepnf  31792  nmfnrepnf  31805  pjssposi  32097  cvcon3  32209  mdsymlem8  32335  dmdsym  32338  disjunsn  32505  fimarab  32551  unipreima  32552  fmptcof2  32565  ressupprn  32593  1stpreima  32609  fpwrelmapffslem  32637  infxrge0gelb  32659  nndiffz1  32677  mgccnv  32857  pwrssmgc  32858  cntzun  32906  isinftm  33023  qusxpid  33215  lindfpropd  33234  lindspropd  33235  unitprodclb  33241  lsmssass  33254  nsgmgc  33264  crngmxidl  33321  opprqusdrng  33345  qsfld  33350  ply1dg1rt  33426  finexttrb  33523  algextdeglem7  33560  ist0cld  33604  metidv  33663  metider  33665  pstmxmet  33668  xrge0iifiso  33706  indpi1  33809  prodindf  33812  indf1ofs  33815  aean  34033  brfae  34037  signsply0  34353  signsvfn  34384  reprinrn  34420  subfacp1lem3  34962  subfacp1lem5  34964  fmlafvel  35165  opelco3  35546  sscoid  35685  cgrcomr  35769  ofscom  35779  cgr3permute3  35819  cgr3permute1  35820  cgr3com  35825  colinearperm1  35834  colinearperm3  35835  outsideofcom  35900  opnbnd  35985  filnetlem4  36041  finxpsuclem  37052  wl-equsald  37182  wl-equsaldv  37183  lindsadd  37262  poimirlem23  37292  broucube  37303  heicant  37304  itg2addnclem2  37321  ftc1anclem1  37342  ftc1anclem5  37346  ftc1anclem6  37347  areacirclem5  37361  areacirc  37362  caures  37409  cnpwstotbnd  37446  ismtyima  37452  rrnmet  37478  reheibor  37488  rngosn3  37573  brcosscnvcoss  38080  br1cosscnvxrn  38120  eqvrelth  38257  brpartspart  38419  lcvbr  38667  lkrsc  38743  lshpkrlem1  38756  opltcon3b  38850  cmt2N  38896  cmt3N  38897  cvrcon3b  38923  cvrcmp2  38930  cvlexchb2  38977  cvlatexchb2  38981  2llnmj  39207  4atlem3  39243  4atlem9  39250  4atlem10a  39251  4atlem11a  39254  4atlem12a  39257  4at2  39261  2lplnmj  39269  llnexchb2  39516  lautlt  39738  lautcvr  39739  lautco  39744  ltrnatb  39784  ltrneq2  39795  cdlemefrs29pre00  40042  cdlemefrs29cpre1  40045  cdleme32fva  40084  dibglbN  40813  dochsncom  41029  dochkrsat  41102  lspindp5  41417  mapdh8ab  41424  hdmapip0com  41564  fsuppind  42004  dvdsexpb  42072  sn-ltmul2d  42183  prjsprellsp  42202  lzenom  42364  rmxycomplete  42512  fzneg  42577  modabsdifz  42581  jm2.19  42588  pw2f1ocnv  42632  nadd1suc  42995  fzunt  43059  fzuntd  43060  fzunt1d  43061  fzuntgd  43062  sqrtcvallem1  43235  brtrclfv2  43331  rfovcnvf1od  43608  ntrclsfveq1  43664  ntrclsiso  43671  k0004lem2  43752  caofcan  43934  rfcnpre1  44555  rfcnpre2  44567  ellimcabssub0  45175  liminfpnfuz  45374  xlimpnfxnegmnf2  45416  fperdvper  45477  vonvolmbl  46219  readdcnnred  46853  resubcnnred  46854  cndivrenred  46856  requad2  47132  uhgrimisgrgric  47415  clnbgrgrim  47418  lco0  47747  lindslininds  47784  ltsubaddb  47834  ltsubsubb  47835  ltsubadd2b  47836  elbigolo1  47882  dig2bits  47939  rrx2pnedifcoorneorr  48042  mofeu  48152  sepnsepo  48194  lubeldm2d  48229  glbeldm2d  48230  thincsect2  48316  thinccic  48319  postcposALT  48339