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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbccomlem  3825  pr1eqbg  4818  unisucg  6430  fimarab  6945  fvopab3g  6974  fvimacnvALT  7042  respreima  7051  fmptco  7115  fnnfpeq0  7166  cocan1  7279  cocan2  7280  caofidlcan  7702  ordsucelsuc  7806  ordsucsssuc  7807  fnsuppres  8175  smoword  8341  oaword  8522  omword  8543  om00el  8549  oeword  8564  nnaword  8601  nnmword  8607  eldifsucnn  8638  naddss1  8664  naddunif  8668  swoer  8714  erth  8737  brecop  8796  eceqoveq  8808  xpdom2  9048  pw2f1olem  9057  ixpfi2  9295  cantnfrescl  9633  ttrclselem2  9683  rankr1bg  9763  r1pwcl  9807  fseqenlem1  9996  alephord3  10050  alephdom2  10059  engch  10601  fpwwe2lem6  10609  fpwwe2lem8  10611  ltexpi  10875  ltapi  10876  ltmpi  10877  ltsonq  10942  ltmnq  10945  1idpr  11002  addcanpr  11019  axpre-ltadd  11140  axlttri  11269  subsub23  11450  leadd1  11670  ltsub1  11698  ltsub2  11699  leord1  11729  eqord1  11730  lemul1  12058  lediv1  12071  lt2mul2div  12084  lerec  12089  lediv2  12096  le2msq  12106  suprleub  12172  infregelb  12190  ofsubeq0  12206  ofsubge0  12208  indpi1  12223  avgle1  12475  avgle2  12476  cnref1o  13000  xleneg  13235  xnn0lem1lt  13261  xltadd1  13273  xsubge0  13278  xposdif  13279  xltmul1  13309  supxrleub  13343  infxrgelb  13353  iooneg  13489  iccneg  13490  iccsplit  13503  iccshftr  13504  iccshftl  13506  iccdil  13508  icccntr  13510  fzsplit2  13568  fzaddel  13577  fzrev  13606  predfz  13672  elfzo  13680  nelfzo  13684  fzon  13700  elfzom1b  13786  negmod0  13902  leexp2  14198  ltexp2r  14200  repswsymball  14806  repswsymballbi  14807  cjreb  15164  sqrtlt  15302  limsuplt  15520  o1lo1  15578  rlimresb  15606  lo1eq  15609  rlimeq  15610  o1eq  15611  isercoll  15709  efle  16164  tanaddlem  16212  nndivdvds  16309  moddvds  16311  modmulconst  16336  oddm1even  16391  ltoddhalfle  16409  bitsp1  16479  sadcaddlem  16505  sadadd  16515  sadass  16519  bitsshft  16523  smuval2  16530  smumul  16541  dvdssq  16615  phiprmpw  16825  eulerthlem2  16831  odzdvds  16845  pc2dvds  16929  1arith  16977  imasleval  17585  mreacs  17704  catpropd  17755  oppcsect  17825  funcres2b  17944  fthsect  17974  fthinv  17975  fucsect  18022  fucinv  18023  latnlemlt  18518  latnle  18519  ipole  18580  ipolt  18581  mgmpropd  18699  issubg3  19202  eqgid  19239  qusxpid  19242  resghm2b  19295  conjghm  19310  ghmqusker  19348  gastacos  19371  resscntz  19394  cntzrec  19397  oppgsubm  19423  oppgsubg  19424  sylow3lem6  19693  lsmcom2  19716  lsmass  19730  ablsubsub23  19885  lsmcomx  19917  subgdmdprd  20097  opprsubrng  20635  opprsubrg  20669  lsslss  21051  lbspropd  21189  islbs2  21247  rspsn  21461  prmirred  21584  znfld  21670  lindfmm  21937  lindsmm  21938  lsslindf  21940  lsslinds  21941  islindf4  21948  psrbagconf1o  22039  gsumbagdiaglem  22041  mplmonmul  22147  basdif0  23071  neiptopreu  23251  neitr  23298  restlp  23301  cnrest2  23404  cnprest  23407  cnprest2  23408  lmss  23416  lmff  23419  ist1-2  23465  lpcls  23482  perfcls  23483  cmpfi  23526  hauseqlcld  23764  txlm  23766  txkgen  23770  xkopt  23773  idqtop  23824  tgqtop  23830  qtopcn  23832  uffix  24039  fmco  24079  flimrest  24101  lmflf  24123  txflf  24124  fclsrest  24142  cnpfcf  24159  tsmsgsum  24257  tsmsres  24262  tsmsf1o  24263  fmucndlem  24408  ismet2  24451  imasf1oxmet  24493  blres  24549  xmetec  24552  imasf1obl  24606  imasf1oxms  24607  prdsbl  24609  stdbdbl  24635  metrest  24642  metustsym  24673  blval2  24680  metuel2  24683  tngngp  24772  cnbl0  24891  cnblcld  24892  bl2ioo  24910  cncfcnvcn  25045  iihalf2  25053  icoopnst  25059  iocopnst  25060  icopnfcnv  25062  icopnfhmeo  25063  cphorthcom  25321  caucfil  25403  lmclim  25423  cmsss  25471  rrxmet  25528  volsup  25676  dyaddisjlem  25715  mbfeqalem1  25761  mbfeqalem2  25762  mbfeqa  25763  mbfmulc2lem  25767  mbfmax  25769  mbfposr  25772  ismbf3d  25774  mbfimaopnlem  25775  mbfaddlem  25780  mbfsup  25784  mbfinf  25785  0plef  25792  0pledm  25793  i1fmulclem  25822  i1fres  25825  i1fpos  25826  itg1climres  25834  mbfi1fseqlem4  25838  itg2mulclem  25866  itg2monolem1  25870  itg2cnlem1  25881  iblre  25914  iblcn  25919  itgeqa  25934  ellimc2  25997  limcflf  26001  dvreslem  26029  lhop1  26134  r1pid2  26280  ply1remlem  26283  fta1glem2  26287  ofmulrt  26401  plydiveu  26420  plyremlem  26426  quotcan  26431  ulmres  26509  cos11  26656  logleb  26726  argrege0  26734  logdivle  26745  efopn  26781  logccv  26786  cxplt  26817  cxple  26818  cxple2  26820  cxplt2  26821  cxplt3  26823  cxple3  26824  recxpf1lem  26852  logbleb  26906  logblt  26907  angrtmuld  26931  quad2  26962  atans2  27054  rlimcnp  27088  rlimcnp2  27089  rlimcxp  27096  sqff1o  27304  fsumvma2  27336  dchrptlem2  27387  lgsdilem  27446  lgsne0  27457  lgsqr  27473  lgsquadlem1  27502  lgsquadlem2  27503  m1lgs  27510  2lgslem1a  27513  2lgs  27529  dchrisum0lem1  27638  padicabv  27752  nosupinfsep  27854  oldlim  28038  newbday  28053  leslss  28060  ltadds2  28142  lenegs  28197  ltsubs2  28228  ltsubsubsbd  28234  lesubsubsbd  28237  lesubsubs2bd  28238  lesubsubs3bd  28239  lesubsd  28247  lemuls2d  28325  lemuls1d  28326  ltmulnegs1d  28327  onles  28419  n0subs2  28515  bdaypw2bnd  28616  bdayfinbndlem1  28618  trgcgrg  28742  colcom  28785  colrot1  28786  ishlg  28829  hlcomb  28830  hlbtwn  28838  lncom  28849  lnrot2  28851  israg  28928  perpcom  28944  hpgcom  28998  colopp  29000  plngcplem  29015  iscgra  29061  isinag  29090  colinearalglem2  29166  axcgrid  29175  uvtx01vtx  29656  iscplgredg  29676  rgrusgrprc  29848  uspgr2wlkeq  29904  dfpth2  29987  clwlkclwwlk  30262  eupth2lem3lem6  30493  fusgr2wsp2nb  30594  nmorepnf  31029  blocnilem  31065  ubthlem1  31131  shscom  31580  pjpreeq  31659  spansncol  31829  cmcm2  31877  hodsi  32036  nmoprepnf  32128  nmfnrepnf  32141  pjssposi  32433  cvcon3  32545  mdsymlem8  32671  dmdsym  32674  disjunsn  32849  unipreima  32900  fmptcof2  32914  fdifsupp  32942  ressupprn  32947  1stpreima  32964  fpwrelmapffslem  32989  infxrge0gelb  33023  nndiffz1  33043  prodindf  33095  indf1ofs  33099  mgccnv  33232  pwrssmgc  33233  gsumwrd2dccatlem  33310  cntzun  33312  cntrval2  33404  isinftm  33414  domnprodeq0  33512  lindfpropd  33611  lindspropd  33612  unitprodclb  33618  lsmssass  33627  nsgmgc  33637  crngmxidl  33669  opprqusdrng  33692  qsfld  33697  ply1dg1rt  33787  selvply1rhmlemb  33826  psrmonmul  33857  finexttrb  33972  algextdeglem7  34030  ist0cld  34140  metidv  34199  metider  34201  pstmxmet  34204  xrge0iifiso  34242  aean  34551  brfae  34555  signsply0  34855  signsvfn  34886  reprinrn  34922  subfacp1lem3  35545  subfacp1lem5  35547  fmlafvel  35748  opelco3  36138  sscoid  36274  cgrcomr  36360  ofscom  36370  cgr3permute3  36410  cgr3permute1  36411  cgr3com  36416  colinearperm1  36425  colinearperm3  36426  outsideofcom  36491  opnbnd  36698  filnetlem4  36754  finxpsuclem  37903  wl-equsald  38054  wl-equsaldv  38055  lindsadd  38124  poimirlem23  38154  broucube  38165  heicant  38166  itg2addnclem2  38183  ftc1anclem1  38204  ftc1anclem5  38208  ftc1anclem6  38209  areacirclem5  38223  areacirc  38224  caures  38271  cnpwstotbnd  38308  ismtyima  38314  rrnmet  38340  reheibor  38350  rngosn3  38435  ecxrn2  38919  brcosscnvcoss  39035  br1cosscnvxrn  39075  eqvrelth  39206  brpartspart  39387  lcvbr  39657  lkrsc  39733  lshpkrlem1  39746  opltcon3b  39840  cmt2N  39886  cmt3N  39887  cvrcon3b  39913  cvrcmp2  39920  cvlexchb2  39967  cvlatexchb2  39971  2llnmj  40196  4atlem3  40232  4atlem9  40239  4atlem10a  40240  4atlem11a  40243  4atlem12a  40246  4at2  40250  2lplnmj  40258  llnexchb2  40505  lautlt  40727  lautcvr  40728  lautco  40733  ltrnatb  40773  ltrneq2  40784  cdlemefrs29pre00  41031  cdlemefrs29cpre1  41034  cdleme32fva  41073  dibglbN  41802  dochsncom  42018  dochkrsat  42091  lspindp5  42406  mapdh8ab  42413  hdmapip0com  42553  dvdsexpb  42956  sn-ltmul2d  43107  fsuppind  43184  prjsprellsp  43205  lzenom  43363  rmxycomplete  43506  fzneg  43571  modabsdifz  43575  jm2.19  43582  pw2f1ocnv  43626  nadd1suc  43981  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  sqrtcvallem1  44219  brtrclfv2  44315  rfovcnvf1od  44592  ntrclsfveq1  44648  ntrclsiso  44655  k0004lem2  44736  caofcan  44897  rfcnpre1  45597  rfcnpre2  45609  ellimcabssub0  46191  liminfpnfuz  46388  xlimpnfxnegmnf2  46430  fperdvper  46491  vonvolmbl  47233  readdcnnred  47895  resubcnnred  47896  cndivrenred  47898  submodaddmod  47939  minusmodnep2tmod  47951  requad2  48243  uhgrimisgrgric  48551  clnbgrgrim  48554  lco0  49058  lindslininds  49095  ltsubaddb  49145  ltsubsubb  49146  ltsubadd2b  49147  elbigolo1  49188  dig2bits  49245  rrx2pnedifcoorneorr  49348  mofeu  49477  sepnsepo  49553  lubeldm2d  49587  glbeldm2d  49588  cicpropdlem  49678  uptra  49844  uptr2a  49851  thincsect2  50097  thinccic  50100  isinito2lem  50127  postcposALT  50197  lanup  50270  ranup  50271  lmddu  50296