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  3819  pr1eqbg  4813  unisucg  6397  fimarab  6908  fvopab3g  6936  fvimacnvALT  7002  respreima  7011  fmptco  7074  fnnfpeq0  7124  cocan1  7237  cocan2  7238  caofidlcan  7660  ordsucelsuc  7764  ordsucsssuc  7765  fnsuppres  8133  smoword  8298  oaword  8476  omword  8497  om00el  8503  oeword  8518  nnaword  8555  nnmword  8561  eldifsucnn  8592  naddss1  8617  naddunif  8621  swoer  8666  erth  8689  brecop  8747  eceqoveq  8759  xpdom2  9000  pw2f1olem  9009  ixpfi2  9250  cantnfrescl  9585  ttrclselem2  9635  rankr1bg  9715  r1pwcl  9759  fseqenlem1  9934  alephord3  9988  alephdom2  9997  engch  10539  fpwwe2lem6  10547  fpwwe2lem8  10549  ltexpi  10813  ltapi  10814  ltmpi  10815  ltsonq  10880  ltmnq  10883  1idpr  10940  addcanpr  10957  axpre-ltadd  11078  axlttri  11204  subsub23  11385  leadd1  11605  ltsub1  11633  ltsub2  11634  leord1  11664  eqord1  11665  lemul1  11993  lediv1  12007  lt2mul2div  12020  lerec  12025  lediv2  12032  le2msq  12042  suprleub  12108  infregelb  12126  ofsubeq0  12142  ofsubge0  12144  avgle1  12381  avgle2  12382  cnref1o  12898  xleneg  13133  xnn0lem1lt  13159  xltadd1  13171  xsubge0  13176  xposdif  13177  xltmul1  13207  supxrleub  13241  infxrgelb  13251  iooneg  13387  iccneg  13388  iccsplit  13401  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  fzsplit2  13465  fzaddel  13474  fzrev  13503  predfz  13569  elfzo  13577  nelfzo  13580  fzon  13596  elfzom1b  13682  negmod0  13798  leexp2  14094  ltexp2r  14096  repswsymball  14702  repswsymballbi  14703  cjreb  15046  sqrtlt  15184  limsuplt  15402  o1lo1  15460  rlimresb  15488  lo1eq  15491  rlimeq  15492  o1eq  15493  isercoll  15591  efle  16043  tanaddlem  16091  nndivdvds  16188  moddvds  16190  modmulconst  16215  oddm1even  16270  ltoddhalfle  16288  bitsp1  16358  sadcaddlem  16384  sadadd  16394  sadass  16398  bitsshft  16402  smuval2  16409  smumul  16420  dvdssq  16494  phiprmpw  16703  eulerthlem2  16709  odzdvds  16723  pc2dvds  16807  1arith  16855  imasleval  17462  mreacs  17581  catpropd  17632  oppcsect  17702  funcres2b  17821  fthsect  17851  fthinv  17852  fucsect  17899  fucinv  17900  latnlemlt  18395  latnle  18396  ipole  18457  ipolt  18458  mgmpropd  18576  issubg3  19074  eqgid  19109  resghm2b  19163  conjghm  19178  ghmqusker  19216  gastacos  19239  resscntz  19262  cntzrec  19265  oppgsubm  19291  oppgsubg  19292  sylow3lem6  19561  lsmcom2  19584  lsmass  19598  ablsubsub23  19753  lsmcomx  19785  subgdmdprd  19965  opprsubrng  20492  opprsubrg  20526  lsslss  20912  lbspropd  21051  islbs2  21109  rspsn  21288  prmirred  21429  znfld  21515  lindfmm  21782  lindsmm  21783  lsslindf  21785  lsslinds  21786  islindf4  21793  psrbagconf1o  21885  gsumbagdiaglem  21886  mplmonmul  21991  basdif0  22897  neiptopreu  23077  neitr  23124  restlp  23127  cnrest2  23230  cnprest  23233  cnprest2  23234  lmss  23242  lmff  23245  ist1-2  23291  lpcls  23308  perfcls  23309  cmpfi  23352  hauseqlcld  23590  txlm  23592  txkgen  23596  xkopt  23599  idqtop  23650  tgqtop  23656  qtopcn  23658  uffix  23865  fmco  23905  flimrest  23927  lmflf  23949  txflf  23950  fclsrest  23968  cnpfcf  23985  tsmsgsum  24083  tsmsres  24088  tsmsf1o  24089  fmucndlem  24234  ismet2  24277  imasf1oxmet  24319  blres  24375  xmetec  24378  imasf1obl  24432  imasf1oxms  24433  prdsbl  24435  stdbdbl  24461  metrest  24468  metustsym  24499  blval2  24506  metuel2  24509  tngngp  24598  cnbl0  24717  cnblcld  24718  bl2ioo  24736  cncfcnvcn  24875  iihalf2  24884  icoopnst  24892  iocopnst  24893  icopnfcnv  24896  icopnfhmeo  24897  cphorthcom  25157  caucfil  25239  lmclim  25259  cmsss  25307  rrxmet  25364  volsup  25513  dyaddisjlem  25552  mbfeqalem1  25598  mbfeqalem2  25599  mbfeqa  25600  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  ismbf3d  25611  mbfimaopnlem  25612  mbfaddlem  25617  mbfsup  25621  mbfinf  25622  0plef  25629  0pledm  25630  i1fmulclem  25659  i1fres  25662  i1fpos  25663  itg1climres  25671  mbfi1fseqlem4  25675  itg2mulclem  25703  itg2monolem1  25707  itg2cnlem1  25718  iblre  25751  iblcn  25756  itgeqa  25771  ellimc2  25834  limcflf  25838  dvreslem  25866  lhop1  25975  r1pid2  26123  ply1remlem  26126  fta1glem2  26130  ofmulrt  26245  plydiveu  26262  plyremlem  26268  quotcan  26273  ulmres  26353  cos11  26498  logleb  26568  argrege0  26576  logdivle  26587  efopn  26623  logccv  26628  cxplt  26659  cxple  26660  cxple2  26662  cxplt2  26663  cxplt3  26665  cxple3  26666  recxpf1lem  26694  logbleb  26749  logblt  26750  angrtmuld  26774  quad2  26805  atans2  26897  rlimcnp  26931  rlimcnp2  26932  rlimcxp  26940  sqff1o  27148  fsumvma2  27181  dchrptlem2  27232  lgsdilem  27291  lgsne0  27302  lgsqr  27318  lgsquadlem1  27347  lgsquadlem2  27348  m1lgs  27355  2lgslem1a  27358  2lgs  27374  dchrisum0lem1  27483  padicabv  27597  nosupinfsep  27700  oldlim  27883  newbday  27898  leslss  27905  ltadds2  27987  lenegs  28042  ltsubs2  28073  ltsubsubsbd  28079  lesubsubsbd  28082  lesubsubs2bd  28083  lesubsubs3bd  28084  lesubsd  28092  lemuls2d  28170  lemuls1d  28171  ltmulnegs1d  28172  onles  28264  n0subs2  28360  bdaypw2bnd  28461  bdayfinbndlem1  28463  trgcgrg  28587  colcom  28630  colrot1  28631  ishlg  28674  hlcomb  28675  hlbtwn  28683  lncom  28694  lnrot2  28696  israg  28769  perpcom  28785  hpgcom  28839  colopp  28841  iscgra  28881  isinag  28910  colinearalglem2  28980  axcgrid  28989  uvtx01vtx  29470  iscplgredg  29490  rgrusgrprc  29663  uspgr2wlkeq  29719  dfpth2  29802  clwlkclwwlk  30077  eupth2lem3lem6  30308  fusgr2wsp2nb  30409  nmorepnf  30843  blocnilem  30879  ubthlem1  30945  shscom  31394  pjpreeq  31473  spansncol  31643  cmcm2  31691  hodsi  31850  nmoprepnf  31942  nmfnrepnf  31955  pjssposi  32247  cvcon3  32359  mdsymlem8  32485  dmdsym  32488  disjunsn  32669  unipreima  32721  fmptcof2  32735  fdifsupp  32764  ressupprn  32769  1stpreima  32786  fpwrelmapffslem  32811  infxrge0gelb  32846  nndiffz1  32866  indpi1  32941  prodindf  32944  indf1ofs  32948  mgccnv  33081  pwrssmgc  33082  gsumwrd2dccatlem  33159  cntzun  33161  cntrval2  33253  isinftm  33263  domnprodeq0  33358  qusxpid  33444  lindfpropd  33463  lindspropd  33464  unitprodclb  33470  lsmssass  33483  nsgmgc  33493  crngmxidl  33550  opprqusdrng  33574  qsfld  33579  ply1dg1rt  33661  finexttrb  33822  algextdeglem7  33880  ist0cld  33990  metidv  34049  metider  34051  pstmxmet  34054  xrge0iifiso  34092  aean  34401  brfae  34405  signsply0  34708  signsvfn  34739  reprinrn  34775  subfacp1lem3  35376  subfacp1lem5  35378  fmlafvel  35579  opelco3  35969  sscoid  36105  cgrcomr  36191  ofscom  36201  cgr3permute3  36241  cgr3permute1  36242  cgr3com  36247  colinearperm1  36256  colinearperm3  36257  outsideofcom  36322  opnbnd  36519  filnetlem4  36575  finxpsuclem  37598  wl-equsald  37740  wl-equsaldv  37741  lindsadd  37810  poimirlem23  37840  broucube  37851  heicant  37852  itg2addnclem2  37869  ftc1anclem1  37890  ftc1anclem5  37894  ftc1anclem6  37895  areacirclem5  37909  areacirc  37910  caures  37957  cnpwstotbnd  37994  ismtyima  38000  rrnmet  38026  reheibor  38036  rngosn3  38121  ecxrn2  38589  brcosscnvcoss  38693  br1cosscnvxrn  38733  eqvrelth  38864  brpartspart  39028  lcvbr  39277  lkrsc  39353  lshpkrlem1  39366  opltcon3b  39460  cmt2N  39506  cmt3N  39507  cvrcon3b  39533  cvrcmp2  39540  cvlexchb2  39587  cvlatexchb2  39591  2llnmj  39816  4atlem3  39852  4atlem9  39859  4atlem10a  39860  4atlem11a  39863  4atlem12a  39866  4at2  39870  2lplnmj  39878  llnexchb2  40125  lautlt  40347  lautcvr  40348  lautco  40353  ltrnatb  40393  ltrneq2  40404  cdlemefrs29pre00  40651  cdlemefrs29cpre1  40654  cdleme32fva  40693  dibglbN  41422  dochsncom  41638  dochkrsat  41711  lspindp5  42026  mapdh8ab  42033  hdmapip0com  42173  dvdsexpb  42586  sn-ltmul2d  42724  fsuppind  42829  prjsprellsp  42850  lzenom  43008  rmxycomplete  43155  fzneg  43220  modabsdifz  43224  jm2.19  43231  pw2f1ocnv  43275  nadd1suc  43630  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  sqrtcvallem1  43868  brtrclfv2  43964  rfovcnvf1od  44241  ntrclsfveq1  44297  ntrclsiso  44304  k0004lem2  44385  caofcan  44560  rfcnpre1  45260  rfcnpre2  45272  ellimcabssub0  45859  liminfpnfuz  46056  xlimpnfxnegmnf2  46098  fperdvper  46159  vonvolmbl  46901  readdcnnred  47545  resubcnnred  47546  cndivrenred  47548  submodaddmod  47583  minusmodnep2tmod  47595  requad2  47865  uhgrimisgrgric  48173  clnbgrgrim  48176  lco0  48669  lindslininds  48706  ltsubaddb  48756  ltsubsubb  48757  ltsubadd2b  48758  elbigolo1  48799  dig2bits  48856  rrx2pnedifcoorneorr  48959  mofeu  49089  sepnsepo  49165  lubeldm2d  49199  glbeldm2d  49200  cicpropdlem  49290  uptra  49456  uptr2a  49463  thincsect2  49709  thinccic  49712  isinito2lem  49739  postcposALT  49809  lanup  49882  ranup  49883  lmddu  49908