Theorem 3bitr4d 303

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 274	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 271	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  pr1eqbg  4655  fvopab3g  6584  fvimacnvALT  6646  respreima  6655  fmptco  6708  fnnfpeq0  6757  cocan1  6866  cocan2  6867  ordsucelsuc  7347  ordsucsssuc  7348  fnsuppres  7653  smoword  7800  oaword  7968  omword  7989  om00el  7995  oeword  8009  nnaword  8046  nnmword  8052  swoer  8111  erth  8130  brecop  8182  eceqoveq  8194  xpdom2  8400  pw2f1olem  8409  ixpfi2  8609  cantnfrescl  8925  rankr1bg  9018  r1pwcl  9062  fseqenlem1  9236  alephord3  9290  alephdom2  9299  engch  9840  fpwwe2lem7  9848  fpwwe2lem9  9850  ltexpi  10114  ltapi  10115  ltmpi  10116  ltsonq  10181  ltmnq  10184  1idpr  10241  addcanpr  10258  axpre-ltadd  10379  axlttri  10504  subsub23  10683  leadd1  10901  ltsub1  10929  ltsub2  10930  leord1  10960  eqord1  10961  lemul1  11285  lediv1  11298  lt2mul2div  11311  lerec  11316  lediv2  11323  le2msq  11333  suprleub  11400  infregelb  11418  ofsubeq0  11428  ofsubge0  11430  avgle1  11680  avgle2  11681  cnref1o  12192  xleneg  12421  xltadd1  12458  xsubge0  12463  xposdif  12464  xltmul1  12494  supxrleub  12528  infxrgelb  12537  iooneg  12666  iccneg  12667  iccsplit  12680  iccshftr  12681  iccshftl  12683  iccdil  12685  icccntr  12687  fzsplit2  12741  fzaddel  12750  fzrev  12779  predfz  12841  elfzo  12849  nelfzo  12852  fzon  12866  elfzom1b  12944  negmod0  13054  leexp2  13343  ltexp2r  13345  repswsymball  13988  repswsymballbi  13989  cjreb  14333  sqrtlt  14472  limsuplt  14687  o1lo1  14745  rlimresb  14773  lo1eq  14776  rlimeq  14777  o1eq  14778  isercoll  14875  efle  15321  tanaddlem  15369  nndivdvds  15466  moddvds  15468  modmulconst  15491  oddm1even  15542  ltoddhalfle  15560  bitsp1  15630  sadcaddlem  15656  sadadd  15666  sadass  15670  bitsshft  15674  smuval2  15681  smumul  15692  dvdssq  15757  phiprmpw  15959  eulerthlem2  15965  odzdvds  15978  pc2dvds  16061  1arith  16109  imasleval  16660  mreacs  16777  catpropd  16827  oppcsect  16896  funcres2b  17015  fthsect  17043  fthinv  17044  fucsect  17090  fucinv  17091  latnlemlt  17542  latnle  17543  ipole  17616  ipolt  17617  issubg3  18071  eqgid  18105  resghm2b  18137  conjghm  18150  gastacos  18201  resscntz  18223  cntzrec  18225  oppgsubm  18251  oppgsubg  18252  sylow3lem6  18508  lsmcom2  18531  lsmass  18544  ablsubsub23  18693  lsmcomx  18722  subgdmdprd  18896  opprsubrg  19269  lsslss  19445  lbspropd  19583  islbs2  19638  rspsn  19738  psrbagconf1o  19858  gsumbagdiaglem  19859  mplmonmul  19948  prmirred  20334  znfld  20399  lindfmm  20663  lindsmm  20664  lsslindf  20666  lsslinds  20667  islindf4  20674  basdif0  21255  neiptopreu  21435  neitr  21482  restlp  21485  cnrest2  21588  cnprest  21591  cnprest2  21592  lmss  21600  lmff  21603  ist1-2  21649  lpcls  21666  perfcls  21667  cmpfi  21710  hauseqlcld  21948  txlm  21950  txkgen  21954  xkopt  21957  idqtop  22008  tgqtop  22014  qtopcn  22016  uffix  22223  fmco  22263  flimrest  22285  lmflf  22307  txflf  22308  fclsrest  22326  cnpfcf  22343  tsmsgsum  22440  tsmsres  22445  tsmsf1o  22446  fmucndlem  22593  ismet2  22636  imasf1oxmet  22678  blres  22734  xmetec  22737  imasf1obl  22791  imasf1oxms  22792  prdsbl  22794  stdbdbl  22820  metrest  22827  metustsym  22858  blval2  22865  metuel2  22868  tngngp  22956  cnbl0  23075  cnblcld  23076  bl2ioo  23093  cncfcnvcn  23222  iihalf2  23230  icoopnst  23236  iocopnst  23237  icopnfcnv  23239  icopnfhmeo  23240  cphorthcom  23498  caucfil  23579  lmclim  23599  cmsss  23647  rrxmet  23704  volsup  23850  dyaddisjlem  23889  mbfeqalem1  23935  mbfeqalem2  23936  mbfeqa  23937  mbfmulc2lem  23941  mbfmax  23943  mbfposr  23946  ismbf3d  23948  mbfimaopnlem  23949  mbfaddlem  23954  mbfsup  23958  mbfinf  23959  0plef  23966  0pledm  23967  i1fmulclem  23996  i1fres  23999  i1fpos  24000  itg1climres  24008  mbfi1fseqlem4  24012  itg2mulclem  24040  itg2monolem1  24044  itg2cnlem1  24055  iblre  24087  iblcn  24092  itgeqa  24107  ellimc2  24168  limcflf  24172  dvreslem  24200  lhop1  24304  ply1remlem  24449  fta1glem2  24453  ofmulrt  24564  plydiveu  24580  plyremlem  24586  quotcan  24591  ulmres  24669  cos11  24808  logleb  24877  argrege0  24885  logdivle  24896  efopn  24932  logccv  24937  cxplt  24968  cxple  24969  cxple2  24971  cxplt2  24972  cxplt3  24974  cxple3  24975  logbleb  25052  logblt  25053  angrtmuld  25077  quad2  25108  atans2  25200  rlimcnp  25235  rlimcnp2  25236  rlimcxp  25243  sqff1o  25451  fsumvma2  25482  dchrptlem2  25533  lgsdilem  25592  lgsne0  25603  lgsqr  25619  lgsquadlem1  25648  lgsquadlem2  25649  m1lgs  25656  2lgslem1a  25659  2lgs  25675  dchrisum0lem1  25784  padicabv  25898  trgcgrg  25993  colcom  26036  colrot1  26037  ishlg  26080  hlcomb  26081  hlbtwn  26089  lncom  26100  lnrot2  26102  israg  26175  perpcom  26191  hpgcom  26245  colopp  26247  iscgra  26287  isinag  26317  colinearalglem2  26386  axcgrid  26395  uvtx01vtx  26872  iscplgredg  26892  rgrusgrprc  27064  uspgr2wlkeq  27120  clwlkclwwlk  27498  clwlkclwwlkOLD  27499  eupth2lem3lem6  27753  fusgr2wsp2nb  27858  nmorepnf  28312  blocnilem  28348  ubthlem1  28415  shscom  28867  pjpreeq  28946  spansncol  29116  cmcm2  29164  hodsi  29323  nmoprepnf  29415  nmfnrepnf  29428  pjssposi  29720  cvcon3  29832  mdsymlem8  29958  dmdsym  29961  disjunsn  30100  fimarab  30142  unipreima  30143  fmptcof2  30154  1stpreima  30183  fpwrelmapffslem  30209  infxrge0gelb  30231  xnn0lem1lt  30236  nndiffz1  30250  isinftm  30432  lindfpropd  30569  lindspropd  30570  finexttrb  30637  metidv  30733  metider  30735  pstmxmet  30738  xrge0iifiso  30779  indpi1  30880  prodindf  30883  indf1ofs  30886  aean  31105  brfae  31109  signsply0  31428  signsvfn  31461  reprinrn  31498  subfacp1lem3  31974  subfacp1lem5  31976  opelco3  32478  sscoid  32835  cgrcomr  32919  ofscom  32929  cgr3permute3  32969  cgr3permute1  32970  cgr3com  32975  colinearperm1  32984  colinearperm3  32985  outsideofcom  33050  opnbnd  33134  filnetlem4  33190  finxpsuclem  34054  wl-equsald  34157  lindsadd  34274  poimirlem23  34304  broucube  34315  heicant  34316  itg2addnclem2  34333  ftc1anclem1  34356  ftc1anclem5  34360  ftc1anclem6  34361  areacirclem5  34375  areacirc  34376  caures  34425  cnpwstotbnd  34465  ismtyima  34471  rrnmet  34497  reheibor  34507  rngosn3  34592  brcosscnvcoss  35072  br1cosscnvxrn  35107  eqvrelth  35239  lcvbr  35550  lkrsc  35626  lshpkrlem1  35639  opltcon3b  35733  cmt2N  35779  cmt3N  35780  cvrcon3b  35806  cvrcmp2  35813  cvlexchb2  35860  cvlatexchb2  35864  2llnmj  36089  4atlem3  36125  4atlem9  36132  4atlem10a  36133  4atlem11a  36136  4atlem12a  36139  4at2  36143  2lplnmj  36151  llnexchb2  36398  lautlt  36620  lautcvr  36621  lautco  36626  ltrnatb  36666  ltrneq2  36677  cdlemefrs29pre00  36924  cdlemefrs29cpre1  36927  cdleme32fva  36966  dibglbN  37695  dochsncom  37911  dochkrsat  37984  lspindp5  38299  mapdh8ab  38306  hdmapip0com  38446  prjsprellsp  38613  lzenom  38707  rmxycomplete  38855  fzneg  38920  modabsdifz  38924  jm2.19  38931  pw2f1ocnv  38975  brtrclfv2  39380  rfovcnvf1od  39658  ntrclsfveq1  39718  ntrclsiso  39725  k0004lem2  39806  caofcan  40015  rfcnpre1  40639  rfcnpre2  40651  ellimcabssub0  41275  liminfpnfuz  41474  xlimpnfxnegmnf2  41516  fperdvper  41579  vonvolmbl  42320  readdcnnred  42855  resubcnnred  42856  cndivrenred  42858  requad2  43096  mgmpropd  43350  lco0  43789  lindslininds  43826  ltsubaddb  43877  ltsubsubb  43878  ltsubadd2b  43879  elbigolo1  43925  dig2bits  43982  rrx2pnedifcoorneorr  44012