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  3821  pr1eqbg  4815  unisucg  6405  fimarab  6916  fvopab3g  6944  fvimacnvALT  7011  respreima  7020  fmptco  7084  fnnfpeq0  7134  cocan1  7247  cocan2  7248  caofidlcan  7670  ordsucelsuc  7774  ordsucsssuc  7775  fnsuppres  8143  smoword  8308  oaword  8486  omword  8507  om00el  8513  oeword  8528  nnaword  8565  nnmword  8571  eldifsucnn  8602  naddss1  8627  naddunif  8631  swoer  8677  erth  8700  brecop  8759  eceqoveq  8771  xpdom2  9012  pw2f1olem  9021  ixpfi2  9262  cantnfrescl  9597  ttrclselem2  9647  rankr1bg  9727  r1pwcl  9771  fseqenlem1  9946  alephord3  10000  alephdom2  10009  engch  10551  fpwwe2lem6  10559  fpwwe2lem8  10561  ltexpi  10825  ltapi  10826  ltmpi  10827  ltsonq  10892  ltmnq  10895  1idpr  10952  addcanpr  10969  axpre-ltadd  11090  axlttri  11216  subsub23  11397  leadd1  11617  ltsub1  11645  ltsub2  11646  leord1  11676  eqord1  11677  lemul1  12005  lediv1  12019  lt2mul2div  12032  lerec  12037  lediv2  12044  le2msq  12054  suprleub  12120  infregelb  12138  ofsubeq0  12154  ofsubge0  12156  avgle1  12393  avgle2  12394  cnref1o  12910  xleneg  13145  xnn0lem1lt  13171  xltadd1  13183  xsubge0  13188  xposdif  13189  xltmul1  13219  supxrleub  13253  infxrgelb  13263  iooneg  13399  iccneg  13400  iccsplit  13413  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzsplit2  13477  fzaddel  13486  fzrev  13515  predfz  13581  elfzo  13589  nelfzo  13592  fzon  13608  elfzom1b  13694  negmod0  13810  leexp2  14106  ltexp2r  14108  repswsymball  14714  repswsymballbi  14715  cjreb  15058  sqrtlt  15196  limsuplt  15414  o1lo1  15472  rlimresb  15500  lo1eq  15503  rlimeq  15504  o1eq  15505  isercoll  15603  efle  16055  tanaddlem  16103  nndivdvds  16200  moddvds  16202  modmulconst  16227  oddm1even  16282  ltoddhalfle  16300  bitsp1  16370  sadcaddlem  16396  sadadd  16406  sadass  16410  bitsshft  16414  smuval2  16421  smumul  16432  dvdssq  16506  phiprmpw  16715  eulerthlem2  16721  odzdvds  16735  pc2dvds  16819  1arith  16867  imasleval  17474  mreacs  17593  catpropd  17644  oppcsect  17714  funcres2b  17833  fthsect  17863  fthinv  17864  fucsect  17911  fucinv  17912  latnlemlt  18407  latnle  18408  ipole  18469  ipolt  18470  mgmpropd  18588  issubg3  19086  eqgid  19121  resghm2b  19175  conjghm  19190  ghmqusker  19228  gastacos  19251  resscntz  19274  cntzrec  19277  oppgsubm  19303  oppgsubg  19304  sylow3lem6  19573  lsmcom2  19596  lsmass  19610  ablsubsub23  19765  lsmcomx  19797  subgdmdprd  19977  opprsubrng  20504  opprsubrg  20538  lsslss  20924  lbspropd  21063  islbs2  21121  rspsn  21300  prmirred  21441  znfld  21527  lindfmm  21794  lindsmm  21795  lsslindf  21797  lsslinds  21798  islindf4  21805  psrbagconf1o  21897  gsumbagdiaglem  21898  mplmonmul  22003  basdif0  22909  neiptopreu  23089  neitr  23136  restlp  23139  cnrest2  23242  cnprest  23245  cnprest2  23246  lmss  23254  lmff  23257  ist1-2  23303  lpcls  23320  perfcls  23321  cmpfi  23364  hauseqlcld  23602  txlm  23604  txkgen  23608  xkopt  23611  idqtop  23662  tgqtop  23668  qtopcn  23670  uffix  23877  fmco  23917  flimrest  23939  lmflf  23961  txflf  23962  fclsrest  23980  cnpfcf  23997  tsmsgsum  24095  tsmsres  24100  tsmsf1o  24101  fmucndlem  24246  ismet2  24289  imasf1oxmet  24331  blres  24387  xmetec  24390  imasf1obl  24444  imasf1oxms  24445  prdsbl  24447  stdbdbl  24473  metrest  24480  metustsym  24511  blval2  24518  metuel2  24521  tngngp  24610  cnbl0  24729  cnblcld  24730  bl2ioo  24748  cncfcnvcn  24887  iihalf2  24896  icoopnst  24904  iocopnst  24905  icopnfcnv  24908  icopnfhmeo  24909  cphorthcom  25169  caucfil  25251  lmclim  25271  cmsss  25319  rrxmet  25376  volsup  25525  dyaddisjlem  25564  mbfeqalem1  25610  mbfeqalem2  25611  mbfeqa  25612  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  ismbf3d  25623  mbfimaopnlem  25624  mbfaddlem  25629  mbfsup  25633  mbfinf  25634  0plef  25641  0pledm  25642  i1fmulclem  25671  i1fres  25674  i1fpos  25675  itg1climres  25683  mbfi1fseqlem4  25687  itg2mulclem  25715  itg2monolem1  25719  itg2cnlem1  25730  iblre  25763  iblcn  25768  itgeqa  25783  ellimc2  25846  limcflf  25850  dvreslem  25878  lhop1  25987  r1pid2  26135  ply1remlem  26138  fta1glem2  26142  ofmulrt  26257  plydiveu  26274  plyremlem  26280  quotcan  26285  ulmres  26365  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  26761  logblt  26762  angrtmuld  26786  quad2  26817  atans2  26909  rlimcnp  26943  rlimcnp2  26944  rlimcxp  26952  sqff1o  27160  fsumvma2  27193  dchrptlem2  27244  lgsdilem  27303  lgsne0  27314  lgsqr  27330  lgsquadlem1  27359  lgsquadlem2  27360  m1lgs  27367  2lgslem1a  27370  2lgs  27386  dchrisum0lem1  27495  padicabv  27609  nosupinfsep  27712  oldlim  27895  newbday  27910  leslss  27917  ltadds2  27999  lenegs  28054  ltsubs2  28085  ltsubsubsbd  28091  lesubsubsbd  28094  lesubsubs2bd  28095  lesubsubs3bd  28096  lesubsd  28104  lemuls2d  28182  lemuls1d  28183  ltmulnegs1d  28184  onles  28276  n0subs2  28372  bdaypw2bnd  28473  bdayfinbndlem1  28475  trgcgrg  28599  colcom  28642  colrot1  28643  ishlg  28686  hlcomb  28687  hlbtwn  28695  lncom  28706  lnrot2  28708  israg  28781  perpcom  28797  hpgcom  28851  colopp  28853  iscgra  28893  isinag  28922  colinearalglem2  28992  axcgrid  29001  uvtx01vtx  29482  iscplgredg  29502  rgrusgrprc  29675  uspgr2wlkeq  29731  dfpth2  29814  clwlkclwwlk  30089  eupth2lem3lem6  30320  fusgr2wsp2nb  30421  nmorepnf  30855  blocnilem  30891  ubthlem1  30957  shscom  31406  pjpreeq  31485  spansncol  31655  cmcm2  31703  hodsi  31862  nmoprepnf  31954  nmfnrepnf  31967  pjssposi  32259  cvcon3  32371  mdsymlem8  32497  dmdsym  32500  disjunsn  32680  unipreima  32732  fmptcof2  32746  fdifsupp  32774  ressupprn  32779  1stpreima  32796  fpwrelmapffslem  32821  infxrge0gelb  32856  nndiffz1  32876  indpi1  32951  prodindf  32954  indf1ofs  32958  mgccnv  33091  pwrssmgc  33092  gsumwrd2dccatlem  33170  cntzun  33172  cntrval2  33264  isinftm  33274  domnprodeq0  33369  qusxpid  33455  lindfpropd  33474  lindspropd  33475  unitprodclb  33481  lsmssass  33494  nsgmgc  33504  crngmxidl  33561  opprqusdrng  33585  qsfld  33590  ply1dg1rt  33672  psrmonmul  33726  finexttrb  33842  algextdeglem7  33900  ist0cld  34010  metidv  34069  metider  34071  pstmxmet  34074  xrge0iifiso  34112  aean  34421  brfae  34425  signsply0  34728  signsvfn  34759  reprinrn  34795  subfacp1lem3  35395  subfacp1lem5  35397  fmlafvel  35598  opelco3  35988  sscoid  36124  cgrcomr  36210  ofscom  36220  cgr3permute3  36260  cgr3permute1  36261  cgr3com  36266  colinearperm1  36275  colinearperm3  36276  outsideofcom  36341  opnbnd  36538  filnetlem4  36594  finxpsuclem  37646  wl-equsald  37788  wl-equsaldv  37789  lindsadd  37858  poimirlem23  37888  broucube  37899  heicant  37900  itg2addnclem2  37917  ftc1anclem1  37938  ftc1anclem5  37942  ftc1anclem6  37943  areacirclem5  37957  areacirc  37958  caures  38005  cnpwstotbnd  38042  ismtyima  38048  rrnmet  38074  reheibor  38084  rngosn3  38169  ecxrn2  38653  brcosscnvcoss  38769  br1cosscnvxrn  38809  eqvrelth  38940  brpartspart  39121  lcvbr  39391  lkrsc  39467  lshpkrlem1  39480  opltcon3b  39574  cmt2N  39620  cmt3N  39621  cvrcon3b  39647  cvrcmp2  39654  cvlexchb2  39701  cvlatexchb2  39705  2llnmj  39930  4atlem3  39966  4atlem9  39973  4atlem10a  39974  4atlem11a  39977  4atlem12a  39980  4at2  39984  2lplnmj  39992  llnexchb2  40239  lautlt  40461  lautcvr  40462  lautco  40467  ltrnatb  40507  ltrneq2  40518  cdlemefrs29pre00  40765  cdlemefrs29cpre1  40768  cdleme32fva  40807  dibglbN  41536  dochsncom  41752  dochkrsat  41825  lspindp5  42140  mapdh8ab  42147  hdmapip0com  42287  dvdsexpb  42699  sn-ltmul2d  42837  fsuppind  42942  prjsprellsp  42963  lzenom  43121  rmxycomplete  43268  fzneg  43333  modabsdifz  43337  jm2.19  43344  pw2f1ocnv  43388  nadd1suc  43743  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  sqrtcvallem1  43981  brtrclfv2  44077  rfovcnvf1od  44354  ntrclsfveq1  44410  ntrclsiso  44417  k0004lem2  44498  caofcan  44673  rfcnpre1  45373  rfcnpre2  45385  ellimcabssub0  45971  liminfpnfuz  46168  xlimpnfxnegmnf2  46210  fperdvper  46271  vonvolmbl  47013  readdcnnred  47657  resubcnnred  47658  cndivrenred  47660  submodaddmod  47695  minusmodnep2tmod  47707  requad2  47977  uhgrimisgrgric  48285  clnbgrgrim  48288  lco0  48781  lindslininds  48818  ltsubaddb  48868  ltsubsubb  48869  ltsubadd2b  48870  elbigolo1  48911  dig2bits  48968  rrx2pnedifcoorneorr  49071  mofeu  49201  sepnsepo  49277  lubeldm2d  49311  glbeldm2d  49312  cicpropdlem  49402  uptra  49568  uptr2a  49575  thincsect2  49821  thinccic  49824  isinito2lem  49851  postcposALT  49921  lanup  49994  ranup  49995  lmddu  50020