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  3816  pr1eqbg  4808  unisucg  6391  fimarab  6902  fvopab3g  6930  fvimacnvALT  6996  respreima  7005  fmptco  7068  fnnfpeq0  7118  cocan1  7231  cocan2  7232  caofidlcan  7654  ordsucelsuc  7758  ordsucsssuc  7759  fnsuppres  8127  smoword  8292  oaword  8470  omword  8491  om00el  8497  oeword  8511  nnaword  8548  nnmword  8554  eldifsucnn  8585  naddss1  8610  naddunif  8614  swoer  8659  erth  8682  brecop  8740  eceqoveq  8752  xpdom2  8992  pw2f1olem  9001  ixpfi2  9241  cantnfrescl  9573  ttrclselem2  9623  rankr1bg  9703  r1pwcl  9747  fseqenlem1  9922  alephord3  9976  alephdom2  9985  engch  10526  fpwwe2lem6  10534  fpwwe2lem8  10536  ltexpi  10800  ltapi  10801  ltmpi  10802  ltsonq  10867  ltmnq  10870  1idpr  10927  addcanpr  10944  axpre-ltadd  11065  axlttri  11191  subsub23  11372  leadd1  11592  ltsub1  11620  ltsub2  11621  leord1  11651  eqord1  11652  lemul1  11980  lediv1  11994  lt2mul2div  12007  lerec  12012  lediv2  12019  le2msq  12029  suprleub  12095  infregelb  12113  ofsubeq0  12129  ofsubge0  12131  avgle1  12368  avgle2  12369  cnref1o  12885  xleneg  13119  xnn0lem1lt  13145  xltadd1  13157  xsubge0  13162  xposdif  13163  xltmul1  13193  supxrleub  13227  infxrgelb  13237  iooneg  13373  iccneg  13374  iccsplit  13387  iccshftr  13388  iccshftl  13390  iccdil  13392  icccntr  13394  fzsplit2  13451  fzaddel  13460  fzrev  13489  predfz  13555  elfzo  13563  nelfzo  13566  fzon  13582  elfzom1b  13668  negmod0  13784  leexp2  14080  ltexp2r  14082  repswsymball  14688  repswsymballbi  14689  cjreb  15032  sqrtlt  15170  limsuplt  15388  o1lo1  15446  rlimresb  15474  lo1eq  15477  rlimeq  15478  o1eq  15479  isercoll  15577  efle  16029  tanaddlem  16077  nndivdvds  16174  moddvds  16176  modmulconst  16201  oddm1even  16256  ltoddhalfle  16274  bitsp1  16344  sadcaddlem  16370  sadadd  16380  sadass  16384  bitsshft  16388  smuval2  16395  smumul  16406  dvdssq  16480  phiprmpw  16689  eulerthlem2  16695  odzdvds  16709  pc2dvds  16793  1arith  16841  imasleval  17447  mreacs  17566  catpropd  17617  oppcsect  17687  funcres2b  17806  fthsect  17836  fthinv  17837  fucsect  17884  fucinv  17885  latnlemlt  18380  latnle  18381  ipole  18442  ipolt  18443  mgmpropd  18561  issubg3  19059  eqgid  19094  resghm2b  19148  conjghm  19163  ghmqusker  19201  gastacos  19224  resscntz  19247  cntzrec  19250  oppgsubm  19276  oppgsubg  19277  sylow3lem6  19546  lsmcom2  19569  lsmass  19583  ablsubsub23  19738  lsmcomx  19770  subgdmdprd  19950  opprsubrng  20476  opprsubrg  20510  lsslss  20896  lbspropd  21035  islbs2  21093  rspsn  21272  prmirred  21413  znfld  21499  lindfmm  21766  lindsmm  21767  lsslindf  21769  lsslinds  21770  islindf4  21777  psrbagconf1o  21868  gsumbagdiaglem  21869  mplmonmul  21972  basdif0  22869  neiptopreu  23049  neitr  23096  restlp  23099  cnrest2  23202  cnprest  23205  cnprest2  23206  lmss  23214  lmff  23217  ist1-2  23263  lpcls  23280  perfcls  23281  cmpfi  23324  hauseqlcld  23562  txlm  23564  txkgen  23568  xkopt  23571  idqtop  23622  tgqtop  23628  qtopcn  23630  uffix  23837  fmco  23877  flimrest  23899  lmflf  23921  txflf  23922  fclsrest  23940  cnpfcf  23957  tsmsgsum  24055  tsmsres  24060  tsmsf1o  24061  fmucndlem  24206  ismet2  24249  imasf1oxmet  24291  blres  24347  xmetec  24350  imasf1obl  24404  imasf1oxms  24405  prdsbl  24407  stdbdbl  24433  metrest  24440  metustsym  24471  blval2  24478  metuel2  24481  tngngp  24570  cnbl0  24689  cnblcld  24690  bl2ioo  24708  cncfcnvcn  24847  iihalf2  24856  icoopnst  24864  iocopnst  24865  icopnfcnv  24868  icopnfhmeo  24869  cphorthcom  25129  caucfil  25211  lmclim  25231  cmsss  25279  rrxmet  25336  volsup  25485  dyaddisjlem  25524  mbfeqalem1  25570  mbfeqalem2  25571  mbfeqa  25572  mbfmulc2lem  25576  mbfmax  25578  mbfposr  25581  ismbf3d  25583  mbfimaopnlem  25584  mbfaddlem  25589  mbfsup  25593  mbfinf  25594  0plef  25601  0pledm  25602  i1fmulclem  25631  i1fres  25634  i1fpos  25635  itg1climres  25643  mbfi1fseqlem4  25647  itg2mulclem  25675  itg2monolem1  25679  itg2cnlem1  25690  iblre  25723  iblcn  25728  itgeqa  25743  ellimc2  25806  limcflf  25810  dvreslem  25838  lhop1  25947  r1pid2  26095  ply1remlem  26098  fta1glem2  26102  ofmulrt  26217  plydiveu  26234  plyremlem  26240  quotcan  26245  ulmres  26325  cos11  26470  logleb  26540  argrege0  26548  logdivle  26559  efopn  26595  logccv  26600  cxplt  26631  cxple  26632  cxple2  26634  cxplt2  26635  cxplt3  26637  cxple3  26638  recxpf1lem  26666  logbleb  26721  logblt  26722  angrtmuld  26746  quad2  26777  atans2  26869  rlimcnp  26903  rlimcnp2  26904  rlimcxp  26912  sqff1o  27120  fsumvma2  27153  dchrptlem2  27204  lgsdilem  27263  lgsne0  27274  lgsqr  27290  lgsquadlem1  27319  lgsquadlem2  27320  m1lgs  27327  2lgslem1a  27330  2lgs  27346  dchrisum0lem1  27455  padicabv  27569  nosupinfsep  27672  oldlim  27833  newbday  27848  slelss  27855  sltadd2  27935  sleneg  27989  sltsub2  28018  sltsubsubbd  28024  slesubsubbd  28027  slesubsub2bd  28028  slesubsub3bd  28029  slemul2d  28114  slemul1d  28115  sltmulneg1d  28116  n0subs2  28291  trgcgrg  28494  colcom  28537  colrot1  28538  ishlg  28581  hlcomb  28582  hlbtwn  28590  lncom  28601  lnrot2  28603  israg  28676  perpcom  28692  hpgcom  28746  colopp  28748  iscgra  28788  isinag  28817  colinearalglem2  28887  axcgrid  28896  uvtx01vtx  29377  iscplgredg  29397  rgrusgrprc  29570  uspgr2wlkeq  29626  dfpth2  29709  clwlkclwwlk  29984  eupth2lem3lem6  30215  fusgr2wsp2nb  30316  nmorepnf  30750  blocnilem  30786  ubthlem1  30852  shscom  31301  pjpreeq  31380  spansncol  31550  cmcm2  31598  hodsi  31757  nmoprepnf  31849  nmfnrepnf  31862  pjssposi  32154  cvcon3  32266  mdsymlem8  32392  dmdsym  32395  disjunsn  32576  unipreima  32627  fmptcof2  32641  fdifsupp  32670  ressupprn  32675  1stpreima  32692  fpwrelmapffslem  32719  infxrge0gelb  32753  nndiffz1  32773  indpi1  32848  prodindf  32851  indf1ofs  32854  mgccnv  32987  pwrssmgc  32988  gsumwrd2dccatlem  33053  cntzun  33055  cntrval2  33147  isinftm  33157  qusxpid  33335  lindfpropd  33354  lindspropd  33355  unitprodclb  33361  lsmssass  33374  nsgmgc  33384  crngmxidl  33441  opprqusdrng  33465  qsfld  33470  ply1dg1rt  33550  finexttrb  33699  algextdeglem7  33757  ist0cld  33867  metidv  33926  metider  33928  pstmxmet  33931  xrge0iifiso  33969  aean  34278  brfae  34282  signsply0  34585  signsvfn  34616  reprinrn  34652  subfacp1lem3  35247  subfacp1lem5  35249  fmlafvel  35450  opelco3  35840  sscoid  35976  cgrcomr  36062  ofscom  36072  cgr3permute3  36112  cgr3permute1  36113  cgr3com  36118  colinearperm1  36127  colinearperm3  36128  outsideofcom  36193  opnbnd  36390  filnetlem4  36446  finxpsuclem  37462  wl-equsald  37604  wl-equsaldv  37605  lindsadd  37673  poimirlem23  37703  broucube  37714  heicant  37715  itg2addnclem2  37732  ftc1anclem1  37753  ftc1anclem5  37757  ftc1anclem6  37758  areacirclem5  37772  areacirc  37773  caures  37820  cnpwstotbnd  37857  ismtyima  37863  rrnmet  37889  reheibor  37899  rngosn3  37984  ecxrn2  38452  brcosscnvcoss  38556  br1cosscnvxrn  38596  eqvrelth  38727  brpartspart  38891  lcvbr  39140  lkrsc  39216  lshpkrlem1  39229  opltcon3b  39323  cmt2N  39369  cmt3N  39370  cvrcon3b  39396  cvrcmp2  39403  cvlexchb2  39450  cvlatexchb2  39454  2llnmj  39679  4atlem3  39715  4atlem9  39722  4atlem10a  39723  4atlem11a  39726  4atlem12a  39729  4at2  39733  2lplnmj  39741  llnexchb2  39988  lautlt  40210  lautcvr  40211  lautco  40216  ltrnatb  40256  ltrneq2  40267  cdlemefrs29pre00  40514  cdlemefrs29cpre1  40517  cdleme32fva  40556  dibglbN  41285  dochsncom  41501  dochkrsat  41574  lspindp5  41889  mapdh8ab  41896  hdmapip0com  42036  dvdsexpb  42453  sn-ltmul2d  42591  fsuppind  42708  prjsprellsp  42729  lzenom  42887  rmxycomplete  43034  fzneg  43099  modabsdifz  43103  jm2.19  43110  pw2f1ocnv  43154  nadd1suc  43509  fzunt  43572  fzuntd  43573  fzunt1d  43574  fzuntgd  43575  sqrtcvallem1  43748  brtrclfv2  43844  rfovcnvf1od  44121  ntrclsfveq1  44177  ntrclsiso  44184  k0004lem2  44265  caofcan  44440  rfcnpre1  45140  rfcnpre2  45152  ellimcabssub0  45741  liminfpnfuz  45938  xlimpnfxnegmnf2  45980  fperdvper  46041  vonvolmbl  46783  readdcnnred  47427  resubcnnred  47428  cndivrenred  47430  submodaddmod  47465  minusmodnep2tmod  47477  requad2  47747  uhgrimisgrgric  48055  clnbgrgrim  48058  lco0  48552  lindslininds  48589  ltsubaddb  48639  ltsubsubb  48640  ltsubadd2b  48641  elbigolo1  48682  dig2bits  48739  rrx2pnedifcoorneorr  48842  mofeu  48972  sepnsepo  49048  lubeldm2d  49082  glbeldm2d  49083  cicpropdlem  49174  uptra  49340  uptr2a  49347  thincsect2  49593  thinccic  49596  isinito2lem  49623  postcposALT  49693  lanup  49766  ranup  49767  lmddu  49792