Theorem 3bitr4d 314

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbccomlem  3825  pr1eqbg  4827  unisucg  6448  fimarab  6962  fvopab3g  6991  fvimacnvALT  7059  respreima  7068  fmptco  7132  fnnfpeq0  7183  cocan1  7300  cocan2  7301  caofidlcan  7725  ordsucelsuc  7827  ordsucsssuc  7828  fnsuppres  8196  smoword  8362  oaword  8543  omword  8564  om00el  8570  oeword  8585  nnaword  8622  nnmword  8628  eldifsucnn  8659  naddss1  8685  naddunif  8689  swoer  8735  erth  8758  brecop  8817  eceqoveq  8829  xpdom2  9070  pw2f1olem  9079  ixpfi2  9317  cantnfrescl  9655  ttrclselem2  9705  rankr1bg  9785  r1pwcl  9829  fseqenlem1  10027  alephord3  10081  alephdom2  10090  engch  10631  fpwwe2lem6  10639  fpwwe2lem8  10641  ltexpi  10905  ltapi  10906  ltmpi  10907  ltsonq  10972  ltmnq  10975  1idpr  11032  addcanpr  11049  axpre-ltadd  11170  axlttri  11299  subsub23  11480  leadd1  11700  ltsub1  11728  ltsub2  11729  leord1  11759  eqord1  11760  lemul1  12085  lediv1  12098  lt2mul2div  12111  lerec  12116  lediv2  12123  le2msq  12133  suprleub  12199  infregelb  12217  ofsubeq0  12233  ofsubge0  12235  indpi1  12250  avgle1  12502  avgle2  12503  cnref1o  13027  xleneg  13262  xnn0lem1lt  13288  xltadd1  13300  xsubge0  13305  xposdif  13306  xltmul1  13336  supxrleub  13370  infxrgelb  13380  iooneg  13516  iccneg  13517  iccsplit  13530  iccshftr  13531  iccshftl  13533  iccdil  13535  icccntr  13537  fzsplit2  13596  fzaddel  13605  fzrev  13634  predfz  13700  elfzo  13708  nelfzo  13712  fzon  13728  elfzom1b  13814  negmod0  13931  leexp2  14227  ltexp2r  14229  repswsymball  14842  repswsymballbi  14843  cjreb  15200  sqrtlt  15338  limsuplt  15556  o1lo1  15614  rlimresb  15642  lo1eq  15645  rlimeq  15646  o1eq  15647  isercoll  15745  efle  16199  tanaddlem  16247  nndivdvds  16344  moddvds  16346  modmulconst  16371  oddm1even  16426  ltoddhalfle  16444  bitsp1  16514  sadcaddlem  16540  sadadd  16550  sadass  16554  bitsshft  16558  smuval2  16565  smumul  16576  dvdssq  16650  phiprmpw  16860  eulerthlem2  16866  odzdvds  16880  pc2dvds  16964  1arith  17012  imasleval  17620  mreacs  17739  catpropd  17790  oppcsect  17860  funcres2b  17979  fthsect  18009  fthinv  18010  fucsect  18057  fucinv  18058  latnlemlt  18553  latnle  18554  ipole  18615  ipolt  18616  mgmpropd  18734  issubg3  19242  eqgid  19279  qusxpid  19282  resghm2b  19335  conjghm  19350  ghmqusker  19388  gastacos  19411  resscntz  19434  cntzrec  19437  oppgsubm  19463  oppgsubg  19464  sylow3lem6  19733  lsmcom2  19756  lsmass  19770  ablsubsub23  19925  lsmcomx  19957  subgdmdprd  20137  opprsubrng  20695  opprsubrg  20729  lsslss  21119  lbspropd  21257  islbs2  21315  rspsn  21538  prmirred  21661  znfld  21747  lindfmm  22014  lindsmm  22015  lsslindf  22017  lsslinds  22018  islindf4  22025  psrbagconf1o  22116  gsumbagdiaglem  22118  mplmonmul  22224  basdif0  23147  neiptopreu  23327  neitr  23374  restlp  23377  cnrest2  23480  cnprest  23483  cnprest2  23484  lmss  23492  lmff  23495  ist1-2  23541  lpcls  23558  perfcls  23559  cmpfi  23602  hauseqlcld  23840  txlm  23842  txkgen  23846  xkopt  23849  idqtop  23900  tgqtop  23906  qtopcn  23908  uffix  24115  fmco  24155  flimrest  24177  lmflf  24199  txflf  24200  fclsrest  24218  cnpfcf  24235  tsmsgsum  24333  tsmsres  24338  tsmsf1o  24339  fmucndlem  24484  ismet2  24527  imasf1oxmet  24569  blres  24625  xmetec  24628  imasf1obl  24682  imasf1oxms  24683  prdsbl  24685  stdbdbl  24711  metrest  24718  metustsym  24749  blval2  24756  metuel2  24759  tngngp  24848  cnbl0  24967  cnblcld  24968  bl2ioo  24986  cncfcnvcn  25121  iihalf2  25129  icoopnst  25135  iocopnst  25136  icopnfcnv  25138  icopnfhmeo  25139  cphorthcom  25397  caucfil  25479  lmclim  25499  cmsss  25547  rrxmet  25604  volsup  25752  dyaddisjlem  25791  mbfeqalem1  25837  mbfeqalem2  25838  mbfeqa  25839  mbfmulc2lem  25843  mbfmax  25845  mbfposr  25848  ismbf3d  25850  mbfimaopnlem  25851  mbfaddlem  25856  mbfsup  25860  mbfinf  25861  0plef  25868  0pledm  25869  i1fmulclem  25898  i1fres  25901  i1fpos  25902  itg1climres  25910  mbfi1fseqlem4  25914  itg2mulclem  25942  itg2monolem1  25946  itg2cnlem1  25957  iblre  25990  iblcn  25995  itgeqa  26010  ellimc2  26073  limcflf  26077  dvreslem  26105  lhop1  26210  r1pid2  26356  ply1remlem  26359  fta1glem2  26363  ofmulrt  26477  plydiveu  26496  plyremlem  26502  quotcan  26507  ulmres  26588  cos11  26735  logleb  26805  argrege0  26813  logdivle  26824  efopn  26860  logccv  26865  cxplt  26896  cxple  26897  cxple2  26899  cxplt2  26900  cxplt3  26902  cxple3  26903  recxpf1lem  26931  logbleb  26985  logblt  26986  angrtmuld  27010  quad2  27041  atans2  27133  rlimcnp  27167  rlimcnp2  27168  rlimcxp  27175  sqff1o  27383  fsumvma2  27415  dchrptlem2  27466  lgsdilem  27525  lgsne0  27536  lgsqr  27552  lgsquadlem1  27581  lgsquadlem2  27582  m1lgs  27589  2lgslem1a  27592  2lgs  27608  dchrisum0lem1  27717  padicabv  27831  nosupinfsep  27933  oldlim  28117  newbday  28132  leslss  28139  ltadds2  28221  lenegs  28276  ltsubs2  28307  ltsubsubsbd  28313  lesubsubsbd  28316  lesubsubs2bd  28317  lesubsubs3bd  28318  lesubsd  28326  lemuls2d  28404  lemuls1d  28405  ltmulnegs1d  28406  onles  28498  n0subs2  28594  bdaypw2bnd  28695  bdayfinbndlem1  28697  trgcgrg  28821  colcom  28864  colrot1  28865  ishlg  28911  hlcomb  28912  hlbtwn  28920  lncom  28932  lnrot2  28934  israg  29014  perpcom  29030  hpgcom  29086  colopp  29088  plngcplem  29104  iscgra  29157  isinag  29192  dfprlng3  29235  colinearalglem2  29294  axcgrid  29303  uvtx01vtx  29784  iscplgredg  29804  rgrusgrprc  29976  uspgr2wlkeq  30032  dfpth2  30115  clwlkclwwlk  30390  eupth2lem3lem6  30621  fusgr2wsp2nb  30722  nmorepnf  31157  blocnilem  31193  ubthlem1  31259  shscom  31708  pjpreeq  31787  spansncol  31957  cmcm2  32005  hodsi  32164  nmoprepnf  32256  nmfnrepnf  32269  pjssposi  32561  cvcon3  32673  mdsymlem8  32799  dmdsym  32802  disjunsn  32976  unipreima  33025  fmptcof2  33039  fdifsupp  33067  ressupprn  33072  1stpreima  33089  fpwrelmapffslem  33114  infxrge0gelb  33148  nndiffz1  33168  prodindf  33219  indf1ofs  33223  mgccnv  33350  pwrssmgc  33351  gsumwrd2dccatlem  33428  cntzun  33430  cntrval2  33522  isinftm  33532  domnprodeq0  33630  lindfpropd  33726  lindspropd  33727  unitprodclb  33733  lsmssass  33742  nsgmgc  33752  crngmxidl  33783  opprqusdrng  33806  qsfld  33811  ply1dg1rt  33901  selvply1rhmlemb  33940  psrmonmul  33971  finexttrb  34086  algextdeglem7  34144  ist0cld  34254  metidv  34313  metider  34315  pstmxmet  34318  xrge0iifiso  34356  aean  34666  brfae  34670  signsply0  34970  signsvfn  35001  reprinrn  35037  subfacp1lem3  35695  subfacp1lem5  35697  fmlafvel  35898  opelco3  36288  sscoid  36424  cgrcomr  36510  ofscom  36520  cgr3permute3  36560  cgr3permute1  36561  cgr3com  36566  colinearperm1  36575  colinearperm3  36576  outsideofcom  36641  naddle  36732  opnbnd  36877  filnetlem4  36933  finxpsuclem  38084  wl-equsald  38235  wl-equsaldv  38236  lindsadd  38305  poimirlem23  38335  broucube  38346  heicant  38347  itg2addnclem2  38364  ftc1anclem1  38385  ftc1anclem5  38389  ftc1anclem6  38390  areacirclem5  38404  areacirc  38405  caures  38452  cnpwstotbnd  38489  ismtyima  38495  rrnmet  38521  reheibor  38531  rngosn3  38616  ecxrn2  39098  brcosscnvcoss  39214  br1cosscnvxrn  39254  eqvrelth  39385  brpartspart  39566  lcvbr  39836  lkrsc  39912  lshpkrlem1  39925  opltcon3b  40019  cmt2N  40065  cmt3N  40066  cvrcon3b  40092  cvrcmp2  40099  cvlexchb2  40146  cvlatexchb2  40150  2llnmj  40375  4atlem3  40411  4atlem9  40418  4atlem10a  40419  4atlem11a  40422  4atlem12a  40425  4at2  40429  2lplnmj  40437  llnexchb2  40684  lautlt  40906  lautcvr  40907  lautco  40912  ltrnatb  40952  ltrneq2  40963  cdlemefrs29pre00  41210  cdlemefrs29cpre1  41213  cdleme32fva  41252  dibglbN  41981  dochsncom  42197  dochkrsat  42270  lspindp5  42585  mapdh8ab  42592  hdmapip0com  42732  quadfac  43013  dvdsexpb  43137  sn-ltmul2d  43288  fsuppind  43363  prjsprellsp  43384  lzenom  43542  rmxycomplete  43685  fzneg  43750  modabsdifz  43754  jm2.19  43761  pw2f1ocnv  43805  nadd1suc  44160  fzunt  44222  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  sqrtcvallem1  44398  brtrclfv2  44494  rfovcnvf1od  44771  ntrclsfveq1  44827  ntrclsiso  44834  k0004lem2  44915  caofcan  45074  rfcnpre1  45780  rfcnpre2  45792  ellimcabssub0  46374  liminfpnfuz  46571  xlimpnfxnegmnf2  46613  fperdvper  46674  vonvolmbl  47416  readdcnnred  48081  resubcnnred  48082  cndivrenred  48084  submodaddmod  48125  minusmodnep2tmod  48137  requad2  48429  uhgrimisgrgric  48737  clnbgrgrim  48740  lco0  49248  lindslininds  49285  ltsubaddb  49335  ltsubsubb  49336  ltsubadd2b  49337  elbigolo1  49378  dig2bits  49435  rrx2pnedifcoorneorr  49538  mofeu  49667  sepnsepo  49743  lubeldm2d  49777  glbeldm2d  49778  cicpropdlem  49868  uptra  50034  uptr2a  50041  thincsect2  50287  thinccic  50290  isinito2lem  50317  postcposALT  50387  lanup  50460  ranup  50461  lmddu  50486