Theorem bitr4id 290

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr4id.2	⊢ (𝜓 ↔ 𝜒)
bitr4id.1	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4id	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
2		bitr4id.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	bicomi 224	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 288	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:  baib  535  cad1  1614  necon2abid  2981  reueubd  3397  issetft  3494  reu8  3742  sbc6gOLD  3822  r19.28z  4504  r19.37zv  4508  r19.45zv  4509  r19.44zv  4510  r19.27z  4511  r19.36zv  4513  ralsnsg  4675  eldifvsn  4802  ssunsn2  4832  iunconst  5006  iinconst  5007  iuneqconst  5008  relsng  5814  dmxp  5942  opelres  6006  ordsseleq  6415  ordequn  6489  funssres  6612  fncnv  6641  ffrnbd  6752  fresaun  6780  dff1o5  6858  tz6.12c  6929  funimass4  6973  fndmdifeq0  7064  fneqeql2  7067  unpreima  7083  dffo3  7122  dffo3f  7126  fnnfpeq0  7198  funfvima  7250  f1eqcocnv  7321  fliftf  7335  isocnv3  7352  isomin  7357  eloprabga  7541  eloprabgaOLD  7542  mpo2eqb  7565  elpwun  7788  dfom2  7889  opabex3d  7989  opabex3rd  7990  opabex3  7991  f1oweALT  7996  fnwelem  8155  mptsuppd  8211  dfrecs3  8411  dfrecs3OLD  8412  oe0m1  8558  oarec  8599  eldifsucnn  8701  naddsuc2  8738  boxcutc  8980  ordunifi  9324  ttrclselem2  9764  r1fin  9811  rankr1c  9859  iscard  10013  iscard2  10014  cardval2  10029  dfac3  10159  kmlem8  10196  infinf  10604  xrlenlt  11324  ltxrlt  11329  negcon2  11560  mulne0b  11902  dfinfre  12247  crne0  12257  elznn  12627  zmax  12985  elfznelfzo  13808  modmuladdnn0  13953  hashneq0  14400  xpcogend  15010  sqrtneglem  15302  rexfiuz  15383  rexanuz2  15385  sumsplit  15801  fsum2dlem  15803  odd2np1  16375  divalgb  16438  gcdcllem2  16534  mrcidb2  17663  fncnvimaeqv  18175  qusecsub  19868  domnmuln0  20726  acsfn1p  20817  lbsacsbs  21176  islpir2  21358  islinds2  21851  islbs4  21870  mplcoe1  22073  mplcoe5  22076  mamucl  22421  mavmulcl  22569  mdetunilem8  22641  iscld4  23089  isconn2  23438  kgencn  23580  tx1cn  23633  tx2cn  23634  elmptrab  23851  isfbas  23853  fbfinnfr  23865  cnfcf  24066  fmucndlem  24316  prdsxmslem2  24558  blval2  24591  cnbl0  24810  cnblcld  24811  metcld  25354  ismbf  25677  ismbfcn  25678  itg1val2  25733  itg2split  25799  itg2monolem1  25800  aannenlem1  26385  pilem1  26510  sinq34lt0t  26566  ellogrn  26616  logeftb  26640  gausslemma2dlem1a  27424  elznns  28403  readdscl  28446  ercgrg  28540  elntg2  29015  usgredgffibi  29356  vtxd0nedgb  29521  vdiscusgrb  29563  upgrspthswlk  29771  s3wwlks2on  29986  clwwlknonwwlknonb  30135  frgrncvvdeqlem2  30329  ch0pss  31474  h1de2ctlem  31584  adjsym  31862  eigposi  31865  dfadj2  31914  elnlfn  31957  xppreima  32662  1stpreima  32722  2ndpreima  32723  creq0  32753  hashgt1  32818  isunit3  33231  isdrng4  33279  qusxpid  33371  lindflbs  33387  dvdsruassoi  33392  dvdsruasso  33393  dvdsrspss  33395  unitprodclb  33397  lsmsnorb  33399  nsgqusf1olem3  33423  qsfld  33506  qtophaus  33797  prsdm  33875  prsrn  33876  1stmbfm  34242  2ndmbfm  34243  eulerpartlemn  34363  reprdifc  34621  circlemeth  34634  bnj1454  34835  bnj984  34945  dffun10  35896  hfext  36165  isfne4b  36324  neifg  36354  taupilem3  37302  topdifinfindis  37329  topdifinffinlem  37330  finxpsuclem  37380  nlpineqsn  37391  wl-ifp-ncond1  37447  poimirlem23  37630  poimirlem26  37633  cnambfre  37655  0totbnd  37760  suceqsneq  38218  opelvvdif  38241  inecmo  38337  brxrn  38356  brin2  38391  eleccossin  38465  dffunsALTV2  38666  dffunsALTV3  38667  dffunsALTV4  38668  elfunsALTV2  38675  elfunsALTV3  38676  elfunsALTV4  38677  elfunsALTV5  38678  dfdisjs2  38691  eldisjs2  38705  disjres  38726  cvrval2  39256  cvrnbtwn2  39257  cvrnbtwn4  39261  hlateq  39382  islpln5  39518  islvol5  39562  pmap11  39745  4atex  40059  cdleme0ex2N  40207  cdlemefrs29pre00  40378  diaord  41030  dihmeetlem13N  41302  lcfl1  41475  lcfls1N  41518  mapdpglem3  41658  isnacs2  42694  mrefg3  42696  pw2f1ocnv  43026  unielss  43207  onmaxnelsup  43212  onsupnmax  43217  onov0suclim  43264  cantnf2  43315  ordsssucb  43325  relexp0eq  43691  frege124d  43751  uneqsn  44015  k0004lem1  44137  sbcoreleleq  44533  r19.28zf  45102  climreeq  45569  funressnfv  46993  fmtnorec2lem  47467  sclnbgrelself  47772  gpgedgel  47943  eenglngeehlnmlem1  48587  eenglngeehlnmlem2  48588  rrx2linest2  48594  itsclinecirc0b  48624  map0cor  48685  ipolublem  48775  ipoglblem  48778