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  3808  pr1eqbg  4801  unisucg  6397  fimarab  6908  fvopab3g  6936  fvimacnvALT  7003  respreima  7012  fmptco  7076  fnnfpeq0  7126  cocan1  7239  cocan2  7240  caofidlcan  7662  ordsucelsuc  7766  ordsucsssuc  7767  fnsuppres  8134  smoword  8299  oaword  8477  omword  8498  om00el  8504  oeword  8519  nnaword  8556  nnmword  8562  eldifsucnn  8593  naddss1  8618  naddunif  8622  swoer  8668  erth  8691  brecop  8750  eceqoveq  8762  xpdom2  9003  pw2f1olem  9012  ixpfi2  9253  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  20527  opprsubrg  20561  lsslss  20947  lbspropd  21086  islbs2  21144  rspsn  21323  prmirred  21464  znfld  21550  lindfmm  21817  lindsmm  21818  lsslindf  21820  lsslinds  21821  islindf4  21828  psrbagconf1o  21919  gsumbagdiaglem  21920  mplmonmul  22024  basdif0  22928  neiptopreu  23108  neitr  23155  restlp  23158  cnrest2  23261  cnprest  23264  cnprest2  23265  lmss  23273  lmff  23276  ist1-2  23322  lpcls  23339  perfcls  23340  cmpfi  23383  hauseqlcld  23621  txlm  23623  txkgen  23627  xkopt  23630  idqtop  23681  tgqtop  23687  qtopcn  23689  uffix  23896  fmco  23936  flimrest  23958  lmflf  23980  txflf  23981  fclsrest  23999  cnpfcf  24016  tsmsgsum  24114  tsmsres  24119  tsmsf1o  24120  fmucndlem  24265  ismet2  24308  imasf1oxmet  24350  blres  24406  xmetec  24409  imasf1obl  24463  imasf1oxms  24464  prdsbl  24466  stdbdbl  24492  metrest  24499  metustsym  24530  blval2  24537  metuel2  24540  tngngp  24629  cnbl0  24748  cnblcld  24749  bl2ioo  24767  cncfcnvcn  24902  iihalf2  24910  icoopnst  24916  iocopnst  24917  icopnfcnv  24919  icopnfhmeo  24920  cphorthcom  25178  caucfil  25260  lmclim  25280  cmsss  25328  rrxmet  25385  volsup  25533  dyaddisjlem  25572  mbfeqalem1  25618  mbfeqalem2  25619  mbfeqa  25620  mbfmulc2lem  25624  mbfmax  25626  mbfposr  25629  ismbf3d  25631  mbfimaopnlem  25632  mbfaddlem  25637  mbfsup  25641  mbfinf  25642  0plef  25649  0pledm  25650  i1fmulclem  25679  i1fres  25682  i1fpos  25683  itg1climres  25691  mbfi1fseqlem4  25695  itg2mulclem  25723  itg2monolem1  25727  itg2cnlem1  25738  iblre  25771  iblcn  25776  itgeqa  25791  ellimc2  25854  limcflf  25858  dvreslem  25886  lhop1  25991  r1pid2  26137  ply1remlem  26140  fta1glem2  26144  ofmulrt  26258  plydiveu  26275  plyremlem  26281  quotcan  26286  ulmres  26366  cos11  26510  logleb  26580  argrege0  26588  logdivle  26599  efopn  26635  logccv  26640  cxplt  26671  cxple  26672  cxple2  26674  cxplt2  26675  cxplt3  26677  cxple3  26678  recxpf1lem  26706  logbleb  26760  logblt  26761  angrtmuld  26785  quad2  26816  atans2  26908  rlimcnp  26942  rlimcnp2  26943  rlimcxp  26951  sqff1o  27159  fsumvma2  27191  dchrptlem2  27242  lgsdilem  27301  lgsne0  27312  lgsqr  27328  lgsquadlem1  27357  lgsquadlem2  27358  m1lgs  27365  2lgslem1a  27368  2lgs  27384  dchrisum0lem1  27493  padicabv  27607  nosupinfsep  27710  oldlim  27893  newbday  27908  leslss  27915  ltadds2  27997  lenegs  28052  ltsubs2  28083  ltsubsubsbd  28089  lesubsubsbd  28092  lesubsubs2bd  28093  lesubsubs3bd  28094  lesubsd  28102  lemuls2d  28180  lemuls1d  28181  ltmulnegs1d  28182  onles  28274  n0subs2  28370  bdaypw2bnd  28471  bdayfinbndlem1  28473  trgcgrg  28597  colcom  28640  colrot1  28641  ishlg  28684  hlcomb  28685  hlbtwn  28693  lncom  28704  lnrot2  28706  israg  28779  perpcom  28795  hpgcom  28849  colopp  28851  iscgra  28891  isinag  28920  colinearalglem2  28990  axcgrid  28999  uvtx01vtx  29480  iscplgredg  29500  rgrusgrprc  29673  uspgr2wlkeq  29729  dfpth2  29812  clwlkclwwlk  30087  eupth2lem3lem6  30318  fusgr2wsp2nb  30419  nmorepnf  30854  blocnilem  30890  ubthlem1  30956  shscom  31405  pjpreeq  31484  spansncol  31654  cmcm2  31702  hodsi  31861  nmoprepnf  31953  nmfnrepnf  31966  pjssposi  32258  cvcon3  32370  mdsymlem8  32496  dmdsym  32499  disjunsn  32679  unipreima  32731  fmptcof2  32745  fdifsupp  32773  ressupprn  32778  1stpreima  32795  fpwrelmapffslem  32820  infxrge0gelb  32854  nndiffz1  32874  prodindf  32937  indf1ofs  32941  mgccnv  33074  pwrssmgc  33075  gsumwrd2dccatlem  33153  cntzun  33155  cntrval2  33247  isinftm  33257  domnprodeq0  33352  qusxpid  33438  lindfpropd  33457  lindspropd  33458  unitprodclb  33464  lsmssass  33477  nsgmgc  33487  crngmxidl  33544  opprqusdrng  33568  qsfld  33573  ply1dg1rt  33655  psrmonmul  33709  finexttrb  33825  algextdeglem7  33883  ist0cld  33993  metidv  34052  metider  34054  pstmxmet  34057  xrge0iifiso  34095  aean  34404  brfae  34408  signsply0  34711  signsvfn  34742  reprinrn  34778  subfacp1lem3  35380  subfacp1lem5  35382  fmlafvel  35583  opelco3  35973  sscoid  36109  cgrcomr  36195  ofscom  36205  cgr3permute3  36245  cgr3permute1  36246  cgr3com  36251  colinearperm1  36260  colinearperm3  36261  outsideofcom  36326  opnbnd  36523  filnetlem4  36579  finxpsuclem  37727  wl-equsald  37878  wl-equsaldv  37879  lindsadd  37948  poimirlem23  37978  broucube  37989  heicant  37990  itg2addnclem2  38007  ftc1anclem1  38028  ftc1anclem5  38032  ftc1anclem6  38033  areacirclem5  38047  areacirc  38048  caures  38095  cnpwstotbnd  38132  ismtyima  38138  rrnmet  38164  reheibor  38174  rngosn3  38259  ecxrn2  38743  brcosscnvcoss  38859  br1cosscnvxrn  38899  eqvrelth  39030  brpartspart  39211  lcvbr  39481  lkrsc  39557  lshpkrlem1  39570  opltcon3b  39664  cmt2N  39710  cmt3N  39711  cvrcon3b  39737  cvrcmp2  39744  cvlexchb2  39791  cvlatexchb2  39795  2llnmj  40020  4atlem3  40056  4atlem9  40063  4atlem10a  40064  4atlem11a  40067  4atlem12a  40070  4at2  40074  2lplnmj  40082  llnexchb2  40329  lautlt  40551  lautcvr  40552  lautco  40557  ltrnatb  40597  ltrneq2  40608  cdlemefrs29pre00  40855  cdlemefrs29cpre1  40858  cdleme32fva  40897  dibglbN  41626  dochsncom  41842  dochkrsat  41915  lspindp5  42230  mapdh8ab  42237  hdmapip0com  42377  dvdsexpb  42781  sn-ltmul2d  42932  fsuppind  43037  prjsprellsp  43058  lzenom  43216  rmxycomplete  43363  fzneg  43428  modabsdifz  43432  jm2.19  43439  pw2f1ocnv  43483  nadd1suc  43838  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  sqrtcvallem1  44076  brtrclfv2  44172  rfovcnvf1od  44449  ntrclsfveq1  44505  ntrclsiso  44512  k0004lem2  44593  caofcan  44768  rfcnpre1  45468  rfcnpre2  45480  ellimcabssub0  46065  liminfpnfuz  46262  xlimpnfxnegmnf2  46304  fperdvper  46365  vonvolmbl  47107  readdcnnred  47763  resubcnnred  47764  cndivrenred  47766  submodaddmod  47807  minusmodnep2tmod  47819  requad2  48111  uhgrimisgrgric  48419  clnbgrgrim  48422  lco0  48915  lindslininds  48952  ltsubaddb  49002  ltsubsubb  49003  ltsubadd2b  49004  elbigolo1  49045  dig2bits  49102  rrx2pnedifcoorneorr  49205  mofeu  49335  sepnsepo  49411  lubeldm2d  49445  glbeldm2d  49446  cicpropdlem  49536  uptra  49702  uptr2a  49709  thincsect2  49955  thinccic  49958  isinito2lem  49985  postcposALT  50055  lanup  50128  ranup  50129  lmddu  50154