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  3832  pr1eqbg  4821  unisucg  6412  fimarab  6935  fvopab3g  6963  fvimacnvALT  7029  respreima  7038  fmptco  7101  fnnfpeq0  7152  cocan1  7266  cocan2  7267  caofidlcan  7691  ordsucelsuc  7797  ordsucsssuc  7798  fnsuppres  8170  smoword  8335  oaword  8513  omword  8534  om00el  8540  oeword  8554  nnaword  8591  nnmword  8597  eldifsucnn  8628  naddss1  8653  naddunif  8657  swoer  8702  erth  8725  brecop  8783  eceqoveq  8795  xpdom2  9036  pw2f1olem  9045  ixpfi2  9301  cantnfrescl  9629  ttrclselem2  9679  rankr1bg  9756  r1pwcl  9800  fseqenlem1  9977  alephord3  10031  alephdom2  10040  engch  10581  fpwwe2lem6  10589  fpwwe2lem8  10591  ltexpi  10855  ltapi  10856  ltmpi  10857  ltsonq  10922  ltmnq  10925  1idpr  10982  addcanpr  10999  axpre-ltadd  11120  axlttri  11245  subsub23  11426  leadd1  11646  ltsub1  11674  ltsub2  11675  leord1  11705  eqord1  11706  lemul1  12034  lediv1  12048  lt2mul2div  12061  lerec  12066  lediv2  12073  le2msq  12083  suprleub  12149  infregelb  12167  ofsubeq0  12183  ofsubge0  12185  avgle1  12422  avgle2  12423  cnref1o  12944  xleneg  13178  xnn0lem1lt  13204  xltadd1  13216  xsubge0  13221  xposdif  13222  xltmul1  13252  supxrleub  13286  infxrgelb  13296  iooneg  13432  iccneg  13433  iccsplit  13446  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzsplit2  13510  fzaddel  13519  fzrev  13548  predfz  13614  elfzo  13622  nelfzo  13625  fzon  13641  elfzom1b  13727  negmod0  13840  leexp2  14136  ltexp2r  14138  repswsymball  14744  repswsymballbi  14745  cjreb  15089  sqrtlt  15227  limsuplt  15445  o1lo1  15503  rlimresb  15531  lo1eq  15534  rlimeq  15535  o1eq  15536  isercoll  15634  efle  16086  tanaddlem  16134  nndivdvds  16231  moddvds  16233  modmulconst  16258  oddm1even  16313  ltoddhalfle  16331  bitsp1  16401  sadcaddlem  16427  sadadd  16437  sadass  16441  bitsshft  16445  smuval2  16452  smumul  16463  dvdssq  16537  phiprmpw  16746  eulerthlem2  16752  odzdvds  16766  pc2dvds  16850  1arith  16898  imasleval  17504  mreacs  17619  catpropd  17670  oppcsect  17740  funcres2b  17859  fthsect  17889  fthinv  17890  fucsect  17937  fucinv  17938  latnlemlt  18431  latnle  18432  ipole  18493  ipolt  18494  mgmpropd  18578  issubg3  19076  eqgid  19112  resghm2b  19166  conjghm  19181  ghmqusker  19219  gastacos  19242  resscntz  19265  cntzrec  19268  oppgsubm  19294  oppgsubg  19295  sylow3lem6  19562  lsmcom2  19585  lsmass  19599  ablsubsub23  19754  lsmcomx  19786  subgdmdprd  19966  opprsubrng  20468  opprsubrg  20502  lsslss  20867  lbspropd  21006  islbs2  21064  rspsn  21243  prmirred  21384  znfld  21470  lindfmm  21736  lindsmm  21737  lsslindf  21739  lsslinds  21740  islindf4  21747  psrbagconf1o  21838  gsumbagdiaglem  21839  mplmonmul  21943  basdif0  22840  neiptopreu  23020  neitr  23067  restlp  23070  cnrest2  23173  cnprest  23176  cnprest2  23177  lmss  23185  lmff  23188  ist1-2  23234  lpcls  23251  perfcls  23252  cmpfi  23295  hauseqlcld  23533  txlm  23535  txkgen  23539  xkopt  23542  idqtop  23593  tgqtop  23599  qtopcn  23601  uffix  23808  fmco  23848  flimrest  23870  lmflf  23892  txflf  23893  fclsrest  23911  cnpfcf  23928  tsmsgsum  24026  tsmsres  24031  tsmsf1o  24032  fmucndlem  24178  ismet2  24221  imasf1oxmet  24263  blres  24319  xmetec  24322  imasf1obl  24376  imasf1oxms  24377  prdsbl  24379  stdbdbl  24405  metrest  24412  metustsym  24443  blval2  24450  metuel2  24453  tngngp  24542  cnbl0  24661  cnblcld  24662  bl2ioo  24680  cncfcnvcn  24819  iihalf2  24828  icoopnst  24836  iocopnst  24837  icopnfcnv  24840  icopnfhmeo  24841  cphorthcom  25101  caucfil  25183  lmclim  25203  cmsss  25251  rrxmet  25308  volsup  25457  dyaddisjlem  25496  mbfeqalem1  25542  mbfeqalem2  25543  mbfeqa  25544  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  ismbf3d  25555  mbfimaopnlem  25556  mbfaddlem  25561  mbfsup  25565  mbfinf  25566  0plef  25573  0pledm  25574  i1fmulclem  25603  i1fres  25606  i1fpos  25607  itg1climres  25615  mbfi1fseqlem4  25619  itg2mulclem  25647  itg2monolem1  25651  itg2cnlem1  25662  iblre  25695  iblcn  25700  itgeqa  25715  ellimc2  25778  limcflf  25782  dvreslem  25810  lhop1  25919  r1pid2  26067  ply1remlem  26070  fta1glem2  26074  ofmulrt  26189  plydiveu  26206  plyremlem  26212  quotcan  26217  ulmres  26297  cos11  26442  logleb  26512  argrege0  26520  logdivle  26531  efopn  26567  logccv  26572  cxplt  26603  cxple  26604  cxple2  26606  cxplt2  26607  cxplt3  26609  cxple3  26610  recxpf1lem  26638  logbleb  26693  logblt  26694  angrtmuld  26718  quad2  26749  atans2  26841  rlimcnp  26875  rlimcnp2  26876  rlimcxp  26884  sqff1o  27092  fsumvma2  27125  dchrptlem2  27176  lgsdilem  27235  lgsne0  27246  lgsqr  27262  lgsquadlem1  27291  lgsquadlem2  27292  m1lgs  27299  2lgslem1a  27302  2lgs  27318  dchrisum0lem1  27427  padicabv  27541  nosupinfsep  27644  oldlim  27798  newbday  27813  slelss  27820  sltadd2  27898  sleneg  27952  sltsub2  27981  sltsubsubbd  27987  slesubsubbd  27990  slesubsub2bd  27991  slesubsub3bd  27992  slemul2d  28077  slemul1d  28078  sltmulneg1d  28079  n0subs2  28254  trgcgrg  28442  colcom  28485  colrot1  28486  ishlg  28529  hlcomb  28530  hlbtwn  28538  lncom  28549  lnrot2  28551  israg  28624  perpcom  28640  hpgcom  28694  colopp  28696  iscgra  28736  isinag  28765  colinearalglem2  28834  axcgrid  28843  uvtx01vtx  29324  iscplgredg  29344  rgrusgrprc  29517  uspgr2wlkeq  29574  dfpth2  29659  clwlkclwwlk  29931  eupth2lem3lem6  30162  fusgr2wsp2nb  30263  nmorepnf  30697  blocnilem  30733  ubthlem1  30799  shscom  31248  pjpreeq  31327  spansncol  31497  cmcm2  31545  hodsi  31704  nmoprepnf  31796  nmfnrepnf  31809  pjssposi  32101  cvcon3  32213  mdsymlem8  32339  dmdsym  32342  disjunsn  32523  unipreima  32567  fmptcof2  32581  fdifsupp  32608  ressupprn  32613  1stpreima  32630  fpwrelmapffslem  32655  infxrge0gelb  32689  nndiffz1  32709  indpi1  32783  prodindf  32786  indf1ofs  32789  mgccnv  32925  pwrssmgc  32926  gsumwrd2dccatlem  33006  cntzun  33008  cntrval2  33128  isinftm  33135  qusxpid  33334  lindfpropd  33353  lindspropd  33354  unitprodclb  33360  lsmssass  33373  nsgmgc  33383  crngmxidl  33440  opprqusdrng  33464  qsfld  33469  ply1dg1rt  33548  finexttrb  33660  algextdeglem7  33713  ist0cld  33823  metidv  33882  metider  33884  pstmxmet  33887  xrge0iifiso  33925  aean  34234  brfae  34238  signsply0  34542  signsvfn  34573  reprinrn  34609  subfacp1lem3  35169  subfacp1lem5  35171  fmlafvel  35372  opelco3  35762  sscoid  35901  cgrcomr  35985  ofscom  35995  cgr3permute3  36035  cgr3permute1  36036  cgr3com  36041  colinearperm1  36050  colinearperm3  36051  outsideofcom  36116  opnbnd  36313  filnetlem4  36369  finxpsuclem  37385  wl-equsald  37527  wl-equsaldv  37528  lindsadd  37607  poimirlem23  37637  broucube  37648  heicant  37649  itg2addnclem2  37666  ftc1anclem1  37687  ftc1anclem5  37691  ftc1anclem6  37692  areacirclem5  37706  areacirc  37707  caures  37754  cnpwstotbnd  37791  ismtyima  37797  rrnmet  37823  reheibor  37833  rngosn3  37918  brcosscnvcoss  38425  br1cosscnvxrn  38465  eqvrelth  38602  brpartspart  38765  lcvbr  39014  lkrsc  39090  lshpkrlem1  39103  opltcon3b  39197  cmt2N  39243  cmt3N  39244  cvrcon3b  39270  cvrcmp2  39277  cvlexchb2  39324  cvlatexchb2  39328  2llnmj  39554  4atlem3  39590  4atlem9  39597  4atlem10a  39598  4atlem11a  39601  4atlem12a  39604  4at2  39608  2lplnmj  39616  llnexchb2  39863  lautlt  40085  lautcvr  40086  lautco  40091  ltrnatb  40131  ltrneq2  40142  cdlemefrs29pre00  40389  cdlemefrs29cpre1  40392  cdleme32fva  40431  dibglbN  41160  dochsncom  41376  dochkrsat  41449  lspindp5  41764  mapdh8ab  41771  hdmapip0com  41911  dvdsexpb  42323  sn-ltmul2d  42461  fsuppind  42578  prjsprellsp  42599  lzenom  42758  rmxycomplete  42906  fzneg  42971  modabsdifz  42975  jm2.19  42982  pw2f1ocnv  43026  nadd1suc  43381  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  sqrtcvallem1  43620  brtrclfv2  43716  rfovcnvf1od  43993  ntrclsfveq1  44049  ntrclsiso  44056  k0004lem2  44137  caofcan  44312  rfcnpre1  45013  rfcnpre2  45025  ellimcabssub0  45615  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  fperdvper  45917  vonvolmbl  46659  readdcnnred  47304  resubcnnred  47305  cndivrenred  47307  submodaddmod  47342  minusmodnep2tmod  47354  requad2  47624  uhgrimisgrgric  47931  clnbgrgrim  47934  lco0  48416  lindslininds  48453  ltsubaddb  48503  ltsubsubb  48504  ltsubadd2b  48505  elbigolo1  48546  dig2bits  48603  rrx2pnedifcoorneorr  48706  mofeu  48836  sepnsepo  48912  lubeldm2d  48946  glbeldm2d  48947  cicpropdlem  49038  uptra  49204  uptr2a  49211  thincsect2  49457  thinccic  49460  isinito2lem  49487  postcposALT  49557  lanup  49630  ranup  49631  lmddu  49656