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  3807  pr1eqbg  4800  unisucg  6403  fimarab  6914  fvopab3g  6942  fvimacnvALT  7009  respreima  7018  fmptco  7082  fnnfpeq0  7133  cocan1  7246  cocan2  7247  caofidlcan  7669  ordsucelsuc  7773  ordsucsssuc  7774  fnsuppres  8141  smoword  8306  oaword  8484  omword  8505  om00el  8511  oeword  8526  nnaword  8563  nnmword  8569  eldifsucnn  8600  naddss1  8625  naddunif  8629  swoer  8675  erth  8698  brecop  8757  eceqoveq  8769  xpdom2  9010  pw2f1olem  9019  ixpfi2  9260  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  11217  subsub23  11398  leadd1  11618  ltsub1  11646  ltsub2  11647  leord1  11677  eqord1  11678  lemul1  12007  lediv1  12021  lt2mul2div  12034  lerec  12039  lediv2  12046  le2msq  12056  suprleub  12122  infregelb  12140  ofsubeq0  12156  ofsubge0  12158  indpi1  12173  avgle1  12417  avgle2  12418  cnref1o  12935  xleneg  13170  xnn0lem1lt  13196  xltadd1  13208  xsubge0  13213  xposdif  13214  xltmul1  13244  supxrleub  13278  infxrgelb  13288  iooneg  13424  iccneg  13425  iccsplit  13438  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzsplit2  13503  fzaddel  13512  fzrev  13541  predfz  13607  elfzo  13615  nelfzo  13619  fzon  13635  elfzom1b  13721  negmod0  13837  leexp2  14133  ltexp2r  14135  repswsymball  14741  repswsymballbi  14742  cjreb  15085  sqrtlt  15223  limsuplt  15441  o1lo1  15499  rlimresb  15527  lo1eq  15530  rlimeq  15531  o1eq  15532  isercoll  15630  efle  16085  tanaddlem  16133  nndivdvds  16230  moddvds  16232  modmulconst  16257  oddm1even  16312  ltoddhalfle  16330  bitsp1  16400  sadcaddlem  16426  sadadd  16436  sadass  16440  bitsshft  16444  smuval2  16451  smumul  16462  dvdssq  16536  phiprmpw  16746  eulerthlem2  16752  odzdvds  16766  pc2dvds  16850  1arith  16898  imasleval  17505  mreacs  17624  catpropd  17675  oppcsect  17745  funcres2b  17864  fthsect  17894  fthinv  17895  fucsect  17942  fucinv  17943  latnlemlt  18438  latnle  18439  ipole  18500  ipolt  18501  mgmpropd  18619  issubg3  19120  eqgid  19155  resghm2b  19209  conjghm  19224  ghmqusker  19262  gastacos  19285  resscntz  19308  cntzrec  19311  oppgsubm  19337  oppgsubg  19338  sylow3lem6  19607  lsmcom2  19630  lsmass  19644  ablsubsub23  19799  lsmcomx  19831  subgdmdprd  20011  opprsubrng  20536  opprsubrg  20570  lsslss  20956  lbspropd  21094  islbs2  21152  rspsn  21331  prmirred  21454  znfld  21540  lindfmm  21807  lindsmm  21808  lsslindf  21810  lsslinds  21811  islindf4  21818  psrbagconf1o  21909  gsumbagdiaglem  21910  mplmonmul  22014  basdif0  22918  neiptopreu  23098  neitr  23145  restlp  23148  cnrest2  23251  cnprest  23254  cnprest2  23255  lmss  23263  lmff  23266  ist1-2  23312  lpcls  23329  perfcls  23330  cmpfi  23373  hauseqlcld  23611  txlm  23613  txkgen  23617  xkopt  23620  idqtop  23671  tgqtop  23677  qtopcn  23679  uffix  23886  fmco  23926  flimrest  23948  lmflf  23970  txflf  23971  fclsrest  23989  cnpfcf  24006  tsmsgsum  24104  tsmsres  24109  tsmsf1o  24110  fmucndlem  24255  ismet2  24298  imasf1oxmet  24340  blres  24396  xmetec  24399  imasf1obl  24453  imasf1oxms  24454  prdsbl  24456  stdbdbl  24482  metrest  24489  metustsym  24520  blval2  24527  metuel2  24530  tngngp  24619  cnbl0  24738  cnblcld  24739  bl2ioo  24757  cncfcnvcn  24892  iihalf2  24900  icoopnst  24906  iocopnst  24907  icopnfcnv  24909  icopnfhmeo  24910  cphorthcom  25168  caucfil  25250  lmclim  25270  cmsss  25318  rrxmet  25375  volsup  25523  dyaddisjlem  25562  mbfeqalem1  25608  mbfeqalem2  25609  mbfeqa  25610  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  ismbf3d  25621  mbfimaopnlem  25622  mbfaddlem  25627  mbfsup  25631  mbfinf  25632  0plef  25639  0pledm  25640  i1fmulclem  25669  i1fres  25672  i1fpos  25673  itg1climres  25681  mbfi1fseqlem4  25685  itg2mulclem  25713  itg2monolem1  25717  itg2cnlem1  25728  iblre  25761  iblcn  25766  itgeqa  25781  ellimc2  25844  limcflf  25848  dvreslem  25876  lhop1  25981  r1pid2  26127  ply1remlem  26130  fta1glem2  26134  ofmulrt  26248  plydiveu  26264  plyremlem  26270  quotcan  26275  ulmres  26353  cos11  26497  logleb  26567  argrege0  26575  logdivle  26586  efopn  26622  logccv  26627  cxplt  26658  cxple  26659  cxple2  26661  cxplt2  26662  cxplt3  26664  cxple3  26665  recxpf1lem  26693  logbleb  26747  logblt  26748  angrtmuld  26772  quad2  26803  atans2  26895  rlimcnp  26929  rlimcnp2  26930  rlimcxp  26937  sqff1o  27145  fsumvma2  27177  dchrptlem2  27228  lgsdilem  27287  lgsne0  27298  lgsqr  27314  lgsquadlem1  27343  lgsquadlem2  27344  m1lgs  27351  2lgslem1a  27354  2lgs  27370  dchrisum0lem1  27479  padicabv  27593  nosupinfsep  27696  oldlim  27879  newbday  27894  leslss  27901  ltadds2  27983  lenegs  28038  ltsubs2  28069  ltsubsubsbd  28075  lesubsubsbd  28078  lesubsubs2bd  28079  lesubsubs3bd  28080  lesubsd  28088  lemuls2d  28166  lemuls1d  28167  ltmulnegs1d  28168  onles  28260  n0subs2  28356  bdaypw2bnd  28457  bdayfinbndlem1  28459  trgcgrg  28583  colcom  28626  colrot1  28627  ishlg  28670  hlcomb  28671  hlbtwn  28679  lncom  28690  lnrot2  28692  israg  28765  perpcom  28781  hpgcom  28835  colopp  28837  iscgra  28877  isinag  28906  colinearalglem2  28976  axcgrid  28985  uvtx01vtx  29466  iscplgredg  29486  rgrusgrprc  29658  uspgr2wlkeq  29714  dfpth2  29797  clwlkclwwlk  30072  eupth2lem3lem6  30303  fusgr2wsp2nb  30404  nmorepnf  30839  blocnilem  30875  ubthlem1  30941  shscom  31390  pjpreeq  31469  spansncol  31639  cmcm2  31687  hodsi  31846  nmoprepnf  31938  nmfnrepnf  31951  pjssposi  32243  cvcon3  32355  mdsymlem8  32481  dmdsym  32484  disjunsn  32664  unipreima  32716  fmptcof2  32730  fdifsupp  32758  ressupprn  32763  1stpreima  32780  fpwrelmapffslem  32805  infxrge0gelb  32839  nndiffz1  32859  prodindf  32922  indf1ofs  32926  mgccnv  33059  pwrssmgc  33060  gsumwrd2dccatlem  33138  cntzun  33140  cntrval2  33232  isinftm  33242  domnprodeq0  33337  qusxpid  33423  lindfpropd  33442  lindspropd  33443  unitprodclb  33449  lsmssass  33462  nsgmgc  33472  crngmxidl  33529  opprqusdrng  33553  qsfld  33558  ply1dg1rt  33640  psrmonmul  33694  finexttrb  33809  algextdeglem7  33867  ist0cld  33977  metidv  34036  metider  34038  pstmxmet  34041  xrge0iifiso  34079  aean  34388  brfae  34392  signsply0  34695  signsvfn  34726  reprinrn  34762  subfacp1lem3  35364  subfacp1lem5  35366  fmlafvel  35567  opelco3  35957  sscoid  36093  cgrcomr  36179  ofscom  36189  cgr3permute3  36229  cgr3permute1  36230  cgr3com  36235  colinearperm1  36244  colinearperm3  36245  outsideofcom  36310  opnbnd  36507  filnetlem4  36563  finxpsuclem  37713  wl-equsald  37864  wl-equsaldv  37865  lindsadd  37934  poimirlem23  37964  broucube  37975  heicant  37976  itg2addnclem2  37993  ftc1anclem1  38014  ftc1anclem5  38018  ftc1anclem6  38019  areacirclem5  38033  areacirc  38034  caures  38081  cnpwstotbnd  38118  ismtyima  38124  rrnmet  38150  reheibor  38160  rngosn3  38245  ecxrn2  38729  brcosscnvcoss  38845  br1cosscnvxrn  38885  eqvrelth  39016  brpartspart  39197  lcvbr  39467  lkrsc  39543  lshpkrlem1  39556  opltcon3b  39650  cmt2N  39696  cmt3N  39697  cvrcon3b  39723  cvrcmp2  39730  cvlexchb2  39777  cvlatexchb2  39781  2llnmj  40006  4atlem3  40042  4atlem9  40049  4atlem10a  40050  4atlem11a  40053  4atlem12a  40056  4at2  40060  2lplnmj  40068  llnexchb2  40315  lautlt  40537  lautcvr  40538  lautco  40543  ltrnatb  40583  ltrneq2  40594  cdlemefrs29pre00  40841  cdlemefrs29cpre1  40844  cdleme32fva  40883  dibglbN  41612  dochsncom  41828  dochkrsat  41901  lspindp5  42216  mapdh8ab  42223  hdmapip0com  42363  dvdsexpb  42767  sn-ltmul2d  42918  fsuppind  43023  prjsprellsp  43044  lzenom  43202  rmxycomplete  43345  fzneg  43410  modabsdifz  43414  jm2.19  43421  pw2f1ocnv  43465  nadd1suc  43820  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  sqrtcvallem1  44058  brtrclfv2  44154  rfovcnvf1od  44431  ntrclsfveq1  44487  ntrclsiso  44494  k0004lem2  44575  caofcan  44750  rfcnpre1  45450  rfcnpre2  45462  ellimcabssub0  46047  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  fperdvper  46347  vonvolmbl  47089  readdcnnred  47751  resubcnnred  47752  cndivrenred  47754  submodaddmod  47795  minusmodnep2tmod  47807  requad2  48099  uhgrimisgrgric  48407  clnbgrgrim  48410  lco0  48903  lindslininds  48940  ltsubaddb  48990  ltsubsubb  48991  ltsubadd2b  48992  elbigolo1  49033  dig2bits  49090  rrx2pnedifcoorneorr  49193  mofeu  49323  sepnsepo  49399  lubeldm2d  49433  glbeldm2d  49434  cicpropdlem  49524  uptra  49690  uptr2a  49697  thincsect2  49943  thinccic  49946  isinito2lem  49973  postcposALT  50043  lanup  50116  ranup  50117  lmddu  50142