Theorem 3bitr4d 302

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  pr1eqbg  4577  fvopab3g  6498  fvimacnvALT  6558  respreima  6566  fmptco  6619  fnnfpeq0  6669  cocan1  6770  cocan2  6771  ordsucelsuc  7252  ordsucsssuc  7253  fnsuppres  7557  smoword  7699  oaword  7866  omword  7887  om00el  7893  oeword  7907  nnaword  7944  nnmword  7950  swoer  8009  erth  8026  brecop  8075  eceqoveq  8088  xpdom2  8294  pw2f1olem  8303  ixpfi2  8503  wemapso2lem  8696  cantnfrescl  8820  rankr1bg  8913  r1pwcl  8957  fseqenlem1  9130  alephord3  9184  alephdom2  9193  engch  9735  fpwwe2lem7  9743  fpwwe2lem9  9745  ltexpi  10009  ltapi  10010  ltmpi  10011  ltsonq  10076  ltmnq  10079  1idpr  10136  addcanpr  10153  axpre-ltadd  10273  axlttri  10394  subsub23  10571  leadd1  10781  ltsub1  10809  ltsub2  10810  leord1  10840  eqord1  10841  lemul1  11160  lediv1  11173  lt2mul2div  11186  lerec  11191  lediv2  11198  le2msq  11208  suprleub  11274  infregelb  11292  ofsubeq0  11302  ofsubge0  11304  avgle1  11539  avgle2  11540  cnref1o  12041  xleneg  12267  xltadd1  12304  xsubge0  12309  xposdif  12310  xltmul1  12340  supxrleub  12374  infxrgelb  12383  iooneg  12513  iccneg  12514  iccsplit  12528  iccshftr  12529  iccshftl  12531  iccdil  12533  icccntr  12535  fzsplit2  12589  fzaddel  12598  fzrev  12626  predfz  12688  elfzo  12696  nelfzo  12699  fzon  12713  elfzom1b  12791  negmod0  12901  leexp2  13138  ltexp2r  13140  repswsymball  13750  repswsymballbi  13751  cjreb  14086  sqrtlt  14225  limsuplt  14433  o1lo1  14491  rlimresb  14519  lo1eq  14522  rlimeq  14523  o1eq  14524  isercoll  14621  efle  15068  tanaddlem  15116  nndivdvds  15212  moddvds  15214  modmulconst  15236  oddm1even  15287  ltoddhalfle  15305  bitsp1  15372  sadcaddlem  15398  sadadd  15408  sadass  15412  bitsshft  15416  smuval2  15423  smumul  15434  dvdssq  15499  phiprmpw  15698  eulerthlem2  15704  odzdvds  15717  pc2dvds  15800  1arith  15848  imasleval  16406  mreacs  16523  catpropd  16573  oppcsect  16642  funcres2b  16761  fthsect  16789  fthinv  16790  fucsect  16836  fucinv  16837  latnlemlt  17289  latnle  17290  ipole  17363  ipolt  17364  issubg3  17814  eqgid  17848  resghm2b  17880  conjghm  17893  gastacos  17944  resscntz  17965  cntzrec  17967  oppgsubm  17993  oppgsubg  17994  sylow3lem6  18248  lsmcom2  18271  lsmass  18284  ablsubsub23  18431  lsmcomx  18460  subgdmdprd  18635  opprsubrg  19005  lsslss  19168  lbspropd  19306  islbs2  19363  rspsn  19463  psrbagconf1o  19583  gsumbagdiaglem  19584  mplmonmul  19673  prmirred  20051  znfld  20116  lindfmm  20376  lindsmm  20377  lsslindf  20379  lsslinds  20380  islindf4  20387  basdif0  20971  neiptopreu  21151  neitr  21198  restlp  21201  cnrest2  21304  cnprest  21307  cnprest2  21308  lmss  21316  lmff  21319  ist1-2  21365  lpcls  21382  perfcls  21383  cmpfi  21425  hauseqlcld  21663  txlm  21665  txkgen  21669  xkopt  21672  idqtop  21723  tgqtop  21729  qtopcn  21731  uffix  21938  fmco  21978  flimrest  22000  lmflf  22022  txflf  22023  fclsrest  22041  cnpfcf  22058  tsmsgsum  22155  tsmsres  22160  tsmsf1o  22161  fmucndlem  22308  ismet2  22351  imasf1oxmet  22393  blres  22449  xmetec  22452  imasf1obl  22506  imasf1oxms  22507  prdsbl  22509  stdbdbl  22535  metrest  22542  metustsym  22573  blval2  22580  metuel2  22583  tngngp  22671  cnbl0  22790  cnblcld  22791  bl2ioo  22808  cncfcnvcn  22937  iihalf2  22945  icoopnst  22951  iocopnst  22952  icopnfcnv  22954  icopnfhmeo  22955  cphorthcom  23213  caucfil  23293  lmclim  23313  cmsss  23359  rrxmet  23403  volsup  23537  dyaddisjlem  23576  mbfeqalem1  23622  mbfeqalem2  23623  mbfeqa  23624  mbfmulc2lem  23628  mbfmax  23630  mbfposr  23633  ismbf3d  23635  mbfimaopnlem  23636  mbfaddlem  23641  mbfsup  23645  mbfinf  23646  0plef  23653  0pledm  23654  i1fmulclem  23683  i1fres  23686  i1fpos  23687  itg1climres  23695  mbfi1fseqlem4  23699  itg2mulclem  23727  itg2monolem1  23731  itg2cnlem1  23742  iblre  23774  iblcn  23779  itgeqa  23794  ellimc2  23855  limcflf  23859  dvreslem  23887  lhop1  23991  ply1remlem  24136  fta1glem2  24140  ofmulrt  24251  plydiveu  24267  plyremlem  24273  quotcan  24278  ulmres  24356  cos11  24494  logleb  24563  argrege0  24571  logdivle  24582  efopn  24618  logccv  24623  cxplt  24654  cxple  24655  cxple2  24657  cxplt2  24658  cxplt3  24660  cxple3  24661  logbleb  24735  logblt  24736  angrtmuld  24752  quad2  24780  atans2  24872  rlimcnp  24906  rlimcnp2  24907  rlimcxp  24914  sqff1o  25122  fsumvma2  25153  dchrptlem2  25204  lgsdilem  25263  lgsne0  25274  lgsqr  25290  lgsquadlem1  25319  lgsquadlem2  25320  m1lgs  25327  2lgslem1a  25330  2lgs  25346  dchrisum0lem1  25419  padicabv  25533  trgcgrg  25624  colcom  25667  colrot1  25668  ishlg  25711  hlcomb  25712  hlbtwn  25720  lncom  25731  lnrot2  25733  israg  25806  perpcom  25822  hpgcom  25873  colopp  25875  iscgra  25915  isinag  25943  colinearalglem2  26001  axcgrid  26010  nbgrsymOLD  26480  uvtx01vtx  26518  uvtxa01vtx0OLD  26520  iscplgredg  26541  rgrusgrprc  26713  uspgr2wlkeq  26770  clwlkclwwlk  27145  eupth2lem3lem6  27406  fusgr2wsp2nb  27509  nmorepnf  27951  blocnilem  27987  ubthlem1  28054  shscom  28506  pjpreeq  28585  spansncol  28755  cmcm2  28803  hodsi  28962  nmoprepnf  29054  nmfnrepnf  29067  pjssposi  29359  cvcon3  29471  mdsymlem8  29597  dmdsym  29600  disjunsn  29732  fimarab  29772  unipreima  29773  fmptcof2  29784  1stpreima  29811  fpwrelmapffslem  29834  infxrge0gelb  29858  nndiffz1  29875  isinftm  30060  metidv  30260  metider  30262  pstmxmet  30265  xrge0iifiso  30306  indpi1  30407  prodindf  30410  indf1ofs  30413  aean  30632  brfae  30636  signsply0  30953  signsvfn  30984  reprinrn  31021  subfacp1lem3  31487  subfacp1lem5  31489  opelco3  31998  sscoid  32341  cgrcomr  32425  ofscom  32435  cgr3permute3  32475  cgr3permute1  32476  cgr3com  32481  colinearperm1  32490  colinearperm3  32491  outsideofcom  32556  opnbnd  32641  filnetlem4  32697  finxpsuclem  33550  wl-equsald  33639  poimirlem23  33745  broucube  33756  heicant  33757  itg2addnclem2  33774  ftc1anclem1  33797  ftc1anclem5  33801  ftc1anclem6  33802  areacirclem5  33816  areacirc  33817  caures  33867  cnpwstotbnd  33907  ismtyima  33913  rrnmet  33939  reheibor  33949  rngosn3  34034  brcosscnvcoss  34502  br1cosscnvxrn  34537  lcvbr  34801  lkrsc  34877  lshpkrlem1  34890  opltcon3b  34984  cmt2N  35030  cmt3N  35031  cvrcon3b  35057  cvrcmp2  35064  cvlexchb2  35111  cvlatexchb2  35115  2llnmj  35340  4atlem3  35376  4atlem9  35383  4atlem10a  35384  4atlem11a  35387  4atlem12a  35390  4at2  35394  2lplnmj  35402  llnexchb2  35649  lautlt  35871  lautcvr  35872  lautco  35877  ltrnatb  35917  ltrneq2  35928  cdlemefrs29pre00  36176  cdlemefrs29cpre1  36179  cdleme32fva  36218  dibglbN  36947  dochsncom  37163  dochkrsat  37236  lspindp5  37551  mapdh8ab  37558  hdmapip0com  37698  lzenom  37835  rmxycomplete  37983  fzneg  38050  modabsdifz  38054  jm2.19  38061  pw2f1ocnv  38105  brtrclfv2  38519  rfovcnvf1od  38798  ntrclsfveq1  38858  ntrclsiso  38865  k0004lem2  38946  caofcan  39022  rfcnpre1  39672  rfcnpre2  39684  ellimcabssub0  40329  fperdvper  40613  vonvolmbl  41357  mgmpropd  42343  lco0  42784  lindslininds  42821  ltsubaddb  42872  ltsubsubb  42873  ltsubadd2b  42874  elbigolo1  42919  dig2bits  42976