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  3820  pr1eqbg  4809  unisucg  6386  fimarab  6896  fvopab3g  6924  fvimacnvALT  6990  respreima  6999  fmptco  7062  fnnfpeq0  7112  cocan1  7225  cocan2  7226  caofidlcan  7648  ordsucelsuc  7752  ordsucsssuc  7753  fnsuppres  8121  smoword  8286  oaword  8464  omword  8485  om00el  8491  oeword  8505  nnaword  8542  nnmword  8548  eldifsucnn  8579  naddss1  8604  naddunif  8608  swoer  8653  erth  8676  brecop  8734  eceqoveq  8746  xpdom2  8985  pw2f1olem  8994  ixpfi2  9234  cantnfrescl  9566  ttrclselem2  9616  rankr1bg  9693  r1pwcl  9737  fseqenlem1  9912  alephord3  9966  alephdom2  9975  engch  10516  fpwwe2lem6  10524  fpwwe2lem8  10526  ltexpi  10790  ltapi  10791  ltmpi  10792  ltsonq  10857  ltmnq  10860  1idpr  10917  addcanpr  10934  axpre-ltadd  11055  axlttri  11181  subsub23  11362  leadd1  11582  ltsub1  11610  ltsub2  11611  leord1  11641  eqord1  11642  lemul1  11970  lediv1  11984  lt2mul2div  11997  lerec  12002  lediv2  12009  le2msq  12019  suprleub  12085  infregelb  12103  ofsubeq0  12119  ofsubge0  12121  avgle1  12358  avgle2  12359  cnref1o  12880  xleneg  13114  xnn0lem1lt  13140  xltadd1  13152  xsubge0  13157  xposdif  13158  xltmul1  13188  supxrleub  13222  infxrgelb  13232  iooneg  13368  iccneg  13369  iccsplit  13382  iccshftr  13383  iccshftl  13385  iccdil  13387  icccntr  13389  fzsplit2  13446  fzaddel  13455  fzrev  13484  predfz  13550  elfzo  13558  nelfzo  13561  fzon  13577  elfzom1b  13663  negmod0  13779  leexp2  14075  ltexp2r  14077  repswsymball  14683  repswsymballbi  14684  cjreb  15027  sqrtlt  15165  limsuplt  15383  o1lo1  15441  rlimresb  15469  lo1eq  15472  rlimeq  15473  o1eq  15474  isercoll  15572  efle  16024  tanaddlem  16072  nndivdvds  16169  moddvds  16171  modmulconst  16196  oddm1even  16251  ltoddhalfle  16269  bitsp1  16339  sadcaddlem  16365  sadadd  16375  sadass  16379  bitsshft  16383  smuval2  16390  smumul  16401  dvdssq  16475  phiprmpw  16684  eulerthlem2  16690  odzdvds  16704  pc2dvds  16788  1arith  16836  imasleval  17442  mreacs  17561  catpropd  17612  oppcsect  17682  funcres2b  17801  fthsect  17831  fthinv  17832  fucsect  17879  fucinv  17880  latnlemlt  18375  latnle  18376  ipole  18437  ipolt  18438  mgmpropd  18556  issubg3  19054  eqgid  19090  resghm2b  19144  conjghm  19159  ghmqusker  19197  gastacos  19220  resscntz  19243  cntzrec  19246  oppgsubm  19272  oppgsubg  19273  sylow3lem6  19542  lsmcom2  19565  lsmass  19579  ablsubsub23  19734  lsmcomx  19766  subgdmdprd  19946  opprsubrng  20472  opprsubrg  20506  lsslss  20892  lbspropd  21031  islbs2  21089  rspsn  21268  prmirred  21409  znfld  21495  lindfmm  21762  lindsmm  21763  lsslindf  21765  lsslinds  21766  islindf4  21773  psrbagconf1o  21864  gsumbagdiaglem  21865  mplmonmul  21969  basdif0  22866  neiptopreu  23046  neitr  23093  restlp  23096  cnrest2  23199  cnprest  23202  cnprest2  23203  lmss  23211  lmff  23214  ist1-2  23260  lpcls  23277  perfcls  23278  cmpfi  23321  hauseqlcld  23559  txlm  23561  txkgen  23565  xkopt  23568  idqtop  23619  tgqtop  23625  qtopcn  23627  uffix  23834  fmco  23874  flimrest  23896  lmflf  23918  txflf  23919  fclsrest  23937  cnpfcf  23954  tsmsgsum  24052  tsmsres  24057  tsmsf1o  24058  fmucndlem  24203  ismet2  24246  imasf1oxmet  24288  blres  24344  xmetec  24347  imasf1obl  24401  imasf1oxms  24402  prdsbl  24404  stdbdbl  24430  metrest  24437  metustsym  24468  blval2  24475  metuel2  24478  tngngp  24567  cnbl0  24686  cnblcld  24687  bl2ioo  24705  cncfcnvcn  24844  iihalf2  24853  icoopnst  24861  iocopnst  24862  icopnfcnv  24865  icopnfhmeo  24866  cphorthcom  25126  caucfil  25208  lmclim  25228  cmsss  25276  rrxmet  25333  volsup  25482  dyaddisjlem  25521  mbfeqalem1  25567  mbfeqalem2  25568  mbfeqa  25569  mbfmulc2lem  25573  mbfmax  25575  mbfposr  25578  ismbf3d  25580  mbfimaopnlem  25581  mbfaddlem  25586  mbfsup  25590  mbfinf  25591  0plef  25598  0pledm  25599  i1fmulclem  25628  i1fres  25631  i1fpos  25632  itg1climres  25640  mbfi1fseqlem4  25644  itg2mulclem  25672  itg2monolem1  25676  itg2cnlem1  25687  iblre  25720  iblcn  25725  itgeqa  25740  ellimc2  25803  limcflf  25807  dvreslem  25835  lhop1  25944  r1pid2  26092  ply1remlem  26095  fta1glem2  26099  ofmulrt  26214  plydiveu  26231  plyremlem  26237  quotcan  26242  ulmres  26322  cos11  26467  logleb  26537  argrege0  26545  logdivle  26556  efopn  26592  logccv  26597  cxplt  26628  cxple  26629  cxple2  26631  cxplt2  26632  cxplt3  26634  cxple3  26635  recxpf1lem  26663  logbleb  26718  logblt  26719  angrtmuld  26743  quad2  26774  atans2  26866  rlimcnp  26900  rlimcnp2  26901  rlimcxp  26909  sqff1o  27117  fsumvma2  27150  dchrptlem2  27201  lgsdilem  27260  lgsne0  27271  lgsqr  27287  lgsquadlem1  27316  lgsquadlem2  27317  m1lgs  27324  2lgslem1a  27327  2lgs  27343  dchrisum0lem1  27452  padicabv  27566  nosupinfsep  27669  oldlim  27830  newbday  27845  slelss  27852  sltadd2  27932  sleneg  27986  sltsub2  28015  sltsubsubbd  28021  slesubsubbd  28024  slesubsub2bd  28025  slesubsub3bd  28026  slemul2d  28111  slemul1d  28112  sltmulneg1d  28113  n0subs2  28288  trgcgrg  28491  colcom  28534  colrot1  28535  ishlg  28578  hlcomb  28579  hlbtwn  28587  lncom  28598  lnrot2  28600  israg  28673  perpcom  28689  hpgcom  28743  colopp  28745  iscgra  28785  isinag  28814  colinearalglem2  28883  axcgrid  28892  uvtx01vtx  29373  iscplgredg  29393  rgrusgrprc  29566  uspgr2wlkeq  29622  dfpth2  29705  clwlkclwwlk  29977  eupth2lem3lem6  30208  fusgr2wsp2nb  30309  nmorepnf  30743  blocnilem  30779  ubthlem1  30845  shscom  31294  pjpreeq  31373  spansncol  31543  cmcm2  31591  hodsi  31750  nmoprepnf  31842  nmfnrepnf  31855  pjssposi  32147  cvcon3  32259  mdsymlem8  32385  dmdsym  32388  disjunsn  32569  unipreima  32620  fmptcof2  32634  fdifsupp  32661  ressupprn  32666  1stpreima  32683  fpwrelmapffslem  32710  infxrge0gelb  32744  nndiffz1  32764  indpi1  32836  prodindf  32839  indf1ofs  32842  mgccnv  32975  pwrssmgc  32976  gsumwrd2dccatlem  33041  cntzun  33043  cntrval2  33135  isinftm  33145  qusxpid  33323  lindfpropd  33342  lindspropd  33343  unitprodclb  33349  lsmssass  33362  nsgmgc  33372  crngmxidl  33429  opprqusdrng  33453  qsfld  33458  ply1dg1rt  33538  finexttrb  33673  algextdeglem7  33731  ist0cld  33841  metidv  33900  metider  33902  pstmxmet  33905  xrge0iifiso  33943  aean  34252  brfae  34256  signsply0  34559  signsvfn  34590  reprinrn  34626  subfacp1lem3  35214  subfacp1lem5  35216  fmlafvel  35417  opelco3  35807  sscoid  35946  cgrcomr  36030  ofscom  36040  cgr3permute3  36080  cgr3permute1  36081  cgr3com  36086  colinearperm1  36095  colinearperm3  36096  outsideofcom  36161  opnbnd  36358  filnetlem4  36414  finxpsuclem  37430  wl-equsald  37572  wl-equsaldv  37573  lindsadd  37652  poimirlem23  37682  broucube  37693  heicant  37694  itg2addnclem2  37711  ftc1anclem1  37732  ftc1anclem5  37736  ftc1anclem6  37737  areacirclem5  37751  areacirc  37752  caures  37799  cnpwstotbnd  37836  ismtyima  37842  rrnmet  37868  reheibor  37878  rngosn3  37963  brcosscnvcoss  38470  br1cosscnvxrn  38510  eqvrelth  38647  brpartspart  38810  lcvbr  39059  lkrsc  39135  lshpkrlem1  39148  opltcon3b  39242  cmt2N  39288  cmt3N  39289  cvrcon3b  39315  cvrcmp2  39322  cvlexchb2  39369  cvlatexchb2  39373  2llnmj  39598  4atlem3  39634  4atlem9  39641  4atlem10a  39642  4atlem11a  39645  4atlem12a  39648  4at2  39652  2lplnmj  39660  llnexchb2  39907  lautlt  40129  lautcvr  40130  lautco  40135  ltrnatb  40175  ltrneq2  40186  cdlemefrs29pre00  40433  cdlemefrs29cpre1  40436  cdleme32fva  40475  dibglbN  41204  dochsncom  41420  dochkrsat  41493  lspindp5  41808  mapdh8ab  41815  hdmapip0com  41955  dvdsexpb  42367  sn-ltmul2d  42505  fsuppind  42622  prjsprellsp  42643  lzenom  42802  rmxycomplete  42949  fzneg  43014  modabsdifz  43018  jm2.19  43025  pw2f1ocnv  43069  nadd1suc  43424  fzunt  43487  fzuntd  43488  fzunt1d  43489  fzuntgd  43490  sqrtcvallem1  43663  brtrclfv2  43759  rfovcnvf1od  44036  ntrclsfveq1  44092  ntrclsiso  44099  k0004lem2  44180  caofcan  44355  rfcnpre1  45055  rfcnpre2  45067  ellimcabssub0  45656  liminfpnfuz  45853  xlimpnfxnegmnf2  45895  fperdvper  45956  vonvolmbl  46698  readdcnnred  47333  resubcnnred  47334  cndivrenred  47336  submodaddmod  47371  minusmodnep2tmod  47383  requad2  47653  uhgrimisgrgric  47961  clnbgrgrim  47964  lco0  48458  lindslininds  48495  ltsubaddb  48545  ltsubsubb  48546  ltsubadd2b  48547  elbigolo1  48588  dig2bits  48645  rrx2pnedifcoorneorr  48748  mofeu  48878  sepnsepo  48954  lubeldm2d  48988  glbeldm2d  48989  cicpropdlem  49080  uptra  49246  uptr2a  49253  thincsect2  49499  thinccic  49502  isinito2lem  49529  postcposALT  49599  lanup  49672  ranup  49673  lmddu  49698