Theorem 3bitr4d 312

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  sbccomlem  3801  pr1eqbg  4788  unisucg  6390  fimarab  6901  fvopab3g  6930  fvimacnvALT  6998  respreima  7007  fmptco  7071  fnnfpeq0  7122  cocan1  7235  cocan2  7236  caofidlcan  7658  ordsucelsuc  7762  ordsucsssuc  7763  fnsuppres  8131  smoword  8296  oaword  8474  omword  8495  om00el  8501  oeword  8516  nnaword  8553  nnmword  8559  eldifsucnn  8590  naddss1  8615  naddunif  8619  swoer  8665  erth  8688  brecop  8747  eceqoveq  8759  xpdom2  9000  pw2f1olem  9009  ixpfi2  9250  cantnfrescl  9588  ttrclselem2  9638  rankr1bg  9718  r1pwcl  9762  fseqenlem1  9937  alephord3  9991  alephdom2  10000  engch  10542  fpwwe2lem6  10550  fpwwe2lem8  10552  ltexpi  10816  ltapi  10817  ltmpi  10818  ltsonq  10883  ltmnq  10886  1idpr  10943  addcanpr  10960  axpre-ltadd  11081  axlttri  11208  subsub23  11389  leadd1  11609  ltsub1  11637  ltsub2  11638  leord1  11668  eqord1  11669  lemul1  11998  lediv1  12012  lt2mul2div  12025  lerec  12030  lediv2  12037  le2msq  12047  suprleub  12113  infregelb  12131  ofsubeq0  12147  ofsubge0  12149  indpi1  12164  avgle1  12408  avgle2  12409  cnref1o  12926  xleneg  13161  xnn0lem1lt  13187  xltadd1  13199  xsubge0  13204  xposdif  13205  xltmul1  13235  supxrleub  13269  infxrgelb  13279  iooneg  13415  iccneg  13416  iccsplit  13429  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzsplit2  13494  fzaddel  13503  fzrev  13532  predfz  13598  elfzo  13606  nelfzo  13610  fzon  13626  elfzom1b  13712  negmod0  13828  leexp2  14124  ltexp2r  14126  repswsymball  14732  repswsymballbi  14733  cjreb  15076  sqrtlt  15214  limsuplt  15432  o1lo1  15490  rlimresb  15518  lo1eq  15521  rlimeq  15522  o1eq  15523  isercoll  15621  efle  16076  tanaddlem  16124  nndivdvds  16221  moddvds  16223  modmulconst  16248  oddm1even  16303  ltoddhalfle  16321  bitsp1  16391  sadcaddlem  16417  sadadd  16427  sadass  16431  bitsshft  16435  smuval2  16442  smumul  16453  dvdssq  16527  phiprmpw  16737  eulerthlem2  16743  odzdvds  16757  pc2dvds  16841  1arith  16889  imasleval  17496  mreacs  17615  catpropd  17666  oppcsect  17736  funcres2b  17855  fthsect  17885  fthinv  17886  fucsect  17933  fucinv  17934  latnlemlt  18429  latnle  18430  ipole  18491  ipolt  18492  mgmpropd  18610  issubg3  19111  eqgid  19146  resghm2b  19200  conjghm  19215  ghmqusker  19253  gastacos  19276  resscntz  19299  cntzrec  19302  oppgsubm  19328  oppgsubg  19329  sylow3lem6  19598  lsmcom2  19621  lsmass  19635  ablsubsub23  19790  lsmcomx  19822  subgdmdprd  20002  opprsubrng  20531  opprsubrg  20565  lsslss  20951  lbspropd  21089  islbs2  21147  rspsn  21326  prmirred  21449  znfld  21535  lindfmm  21802  lindsmm  21803  lsslindf  21805  lsslinds  21806  islindf4  21813  psrbagconf1o  21904  gsumbagdiaglem  21906  mplmonmul  22012  basdif0  22936  neiptopreu  23116  neitr  23163  restlp  23166  cnrest2  23269  cnprest  23272  cnprest2  23273  lmss  23281  lmff  23284  ist1-2  23330  lpcls  23347  perfcls  23348  cmpfi  23391  hauseqlcld  23629  txlm  23631  txkgen  23635  xkopt  23638  idqtop  23689  tgqtop  23695  qtopcn  23697  uffix  23904  fmco  23944  flimrest  23966  lmflf  23988  txflf  23989  fclsrest  24007  cnpfcf  24024  tsmsgsum  24122  tsmsres  24127  tsmsf1o  24128  fmucndlem  24273  ismet2  24316  imasf1oxmet  24358  blres  24414  xmetec  24417  imasf1obl  24471  imasf1oxms  24472  prdsbl  24474  stdbdbl  24500  metrest  24507  metustsym  24538  blval2  24545  metuel2  24548  tngngp  24637  cnbl0  24756  cnblcld  24757  bl2ioo  24775  cncfcnvcn  24910  iihalf2  24918  icoopnst  24924  iocopnst  24925  icopnfcnv  24927  icopnfhmeo  24928  cphorthcom  25186  caucfil  25268  lmclim  25288  cmsss  25336  rrxmet  25393  volsup  25541  dyaddisjlem  25580  mbfeqalem1  25626  mbfeqalem2  25627  mbfeqa  25628  mbfmulc2lem  25632  mbfmax  25634  mbfposr  25637  ismbf3d  25639  mbfimaopnlem  25640  mbfaddlem  25645  mbfsup  25649  mbfinf  25650  0plef  25657  0pledm  25658  i1fmulclem  25687  i1fres  25690  i1fpos  25691  itg1climres  25699  mbfi1fseqlem4  25703  itg2mulclem  25731  itg2monolem1  25735  itg2cnlem1  25746  iblre  25779  iblcn  25784  itgeqa  25799  ellimc2  25862  limcflf  25866  dvreslem  25894  lhop1  25999  r1pid2  26145  ply1remlem  26148  fta1glem2  26152  ofmulrt  26266  plydiveu  26282  plyremlem  26288  quotcan  26293  ulmres  26371  cos11  26515  logleb  26585  argrege0  26593  logdivle  26604  efopn  26640  logccv  26645  cxplt  26676  cxple  26677  cxple2  26679  cxplt2  26680  cxplt3  26682  cxple3  26683  recxpf1lem  26711  logbleb  26765  logblt  26766  angrtmuld  26790  quad2  26821  atans2  26913  rlimcnp  26947  rlimcnp2  26948  rlimcxp  26955  sqff1o  27163  fsumvma2  27195  dchrptlem2  27246  lgsdilem  27305  lgsne0  27316  lgsqr  27332  lgsquadlem1  27361  lgsquadlem2  27362  m1lgs  27369  2lgslem1a  27372  2lgs  27388  dchrisum0lem1  27497  padicabv  27611  nosupinfsep  27714  oldlim  27897  newbday  27912  leslss  27919  ltadds2  28001  lenegs  28056  ltsubs2  28087  ltsubsubsbd  28093  lesubsubsbd  28096  lesubsubs2bd  28097  lesubsubs3bd  28098  lesubsd  28106  lemuls2d  28184  lemuls1d  28185  ltmulnegs1d  28186  onles  28278  n0subs2  28374  bdaypw2bnd  28475  bdayfinbndlem1  28477  trgcgrg  28601  colcom  28644  colrot1  28645  ishlg  28688  hlcomb  28689  hlbtwn  28697  lncom  28708  lnrot2  28710  israg  28783  perpcom  28799  hpgcom  28853  colopp  28855  iscgra  28895  isinag  28924  colinearalglem2  28994  axcgrid  29003  uvtx01vtx  29484  iscplgredg  29504  rgrusgrprc  29676  uspgr2wlkeq  29732  dfpth2  29815  clwlkclwwlk  30090  eupth2lem3lem6  30321  fusgr2wsp2nb  30422  nmorepnf  30857  blocnilem  30893  ubthlem1  30959  shscom  31408  pjpreeq  31487  spansncol  31657  cmcm2  31705  hodsi  31864  nmoprepnf  31956  nmfnrepnf  31969  pjssposi  32261  cvcon3  32373  mdsymlem8  32499  dmdsym  32502  disjunsn  32683  unipreima  32735  fmptcof2  32749  fdifsupp  32777  ressupprn  32782  1stpreima  32799  fpwrelmapffslem  32824  infxrge0gelb  32858  nndiffz1  32878  prodindf  32941  indf1ofs  32945  mgccnv  33078  pwrssmgc  33079  gsumwrd2dccatlem  33158  cntzun  33160  cntrval2  33252  isinftm  33262  domnprodeq0  33357  qusxpid  33446  lindfpropd  33465  lindspropd  33466  unitprodclb  33472  lsmssass  33485  nsgmgc  33495  crngmxidl  33552  opprqusdrng  33576  qsfld  33581  ply1dg1rt  33663  selvply1rhmlemb  33703  psrmonmul  33734  finexttrb  33849  algextdeglem7  33907  ist0cld  34017  metidv  34076  metider  34078  pstmxmet  34081  xrge0iifiso  34119  aean  34428  brfae  34432  signsply0  34735  signsvfn  34766  reprinrn  34802  subfacp1lem3  35410  subfacp1lem5  35412  fmlafvel  35613  opelco3  36003  sscoid  36139  cgrcomr  36225  ofscom  36235  cgr3permute3  36275  cgr3permute1  36276  cgr3com  36281  colinearperm1  36290  colinearperm3  36291  outsideofcom  36356  opnbnd  36553  filnetlem4  36609  finxpsuclem  37759  wl-equsald  37910  wl-equsaldv  37911  lindsadd  37980  poimirlem23  38010  broucube  38021  heicant  38022  itg2addnclem2  38039  ftc1anclem1  38060  ftc1anclem5  38064  ftc1anclem6  38065  areacirclem5  38079  areacirc  38080  caures  38127  cnpwstotbnd  38164  ismtyima  38170  rrnmet  38196  reheibor  38206  rngosn3  38291  ecxrn2  38775  brcosscnvcoss  38891  br1cosscnvxrn  38931  eqvrelth  39062  brpartspart  39243  lcvbr  39513  lkrsc  39589  lshpkrlem1  39602  opltcon3b  39696  cmt2N  39742  cmt3N  39743  cvrcon3b  39769  cvrcmp2  39776  cvlexchb2  39823  cvlatexchb2  39827  2llnmj  40052  4atlem3  40088  4atlem9  40095  4atlem10a  40096  4atlem11a  40099  4atlem12a  40102  4at2  40106  2lplnmj  40114  llnexchb2  40361  lautlt  40583  lautcvr  40584  lautco  40589  ltrnatb  40629  ltrneq2  40640  cdlemefrs29pre00  40887  cdlemefrs29cpre1  40890  cdleme32fva  40929  dibglbN  41658  dochsncom  41874  dochkrsat  41947  lspindp5  42262  mapdh8ab  42269  hdmapip0com  42409  dvdsexpb  42812  sn-ltmul2d  42963  fsuppind  43040  prjsprellsp  43061  lzenom  43219  rmxycomplete  43362  fzneg  43427  modabsdifz  43431  jm2.19  43438  pw2f1ocnv  43482  nadd1suc  43837  fzunt  43899  fzuntd  43900  fzunt1d  43901  fzuntgd  43902  sqrtcvallem1  44075  brtrclfv2  44171  rfovcnvf1od  44448  ntrclsfveq1  44504  ntrclsiso  44511  k0004lem2  44592  caofcan  44767  rfcnpre1  45467  rfcnpre2  45479  ellimcabssub0  46062  liminfpnfuz  46259  xlimpnfxnegmnf2  46301  fperdvper  46362  vonvolmbl  47104  readdcnnred  47766  resubcnnred  47767  cndivrenred  47769  submodaddmod  47810  minusmodnep2tmod  47822  requad2  48114  uhgrimisgrgric  48422  clnbgrgrim  48425  lco0  48918  lindslininds  48955  ltsubaddb  49005  ltsubsubb  49006  ltsubadd2b  49007  elbigolo1  49048  dig2bits  49105  rrx2pnedifcoorneorr  49208  mofeu  49338  sepnsepo  49414  lubeldm2d  49448  glbeldm2d  49449  cicpropdlem  49539  uptra  49705  uptr2a  49712  thincsect2  49958  thinccic  49961  isinito2lem  49988  postcposALT  50058  lanup  50131  ranup  50132  lmddu  50157