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  1617  necon2abid  2975  reueubd  3383  issetft  3480  reu8  3721  r19.28z  4478  r19.37zv  4482  r19.45zv  4483  r19.44zv  4484  r19.27z  4485  r19.36zv  4487  ralsnsg  4651  eldifvsn  4778  ssunsn2  4808  iunconst  4982  iinconst  4983  iuneqconst  4984  relsng  5785  dmxp  5913  opelres  5977  ordsseleq  6386  ordequn  6462  funssres  6585  fncnv  6614  ffrnbd  6726  fresaun  6754  dff1o5  6832  tz6.12c  6903  funimass4  6948  fndmdifeq0  7039  fneqeql2  7042  unpreima  7058  dffo3  7097  dffo3f  7101  fnnfpeq0  7175  funfvima  7227  f1eqcocnv  7299  fliftf  7313  isocnv3  7330  isomin  7335  eloprabga  7521  mpo2eqb  7544  elpwun  7768  dfom2  7868  opabex3d  7969  opabex3rd  7970  opabex3  7971  f1oweALT  7976  fnwelem  8135  mptsuppd  8191  dfrecs3  8391  dfrecs3OLD  8392  oe0m1  8538  oarec  8579  eldifsucnn  8681  naddsuc2  8718  boxcutc  8960  ordunifi  9303  ttrclselem2  9745  r1fin  9792  rankr1c  9840  iscard  9994  iscard2  9995  cardval2  10010  dfac3  10140  kmlem8  10177  infinf  10585  xrlenlt  11305  ltxrlt  11310  negcon2  11541  mulne0b  11883  dfinfre  12228  crne0  12238  elznn  12609  zmax  12966  elfznelfzo  13793  modmuladdnn0  13938  hashneq0  14387  xpcogend  14998  sqrtneglem  15290  rexfiuz  15371  rexanuz2  15373  sumsplit  15789  fsum2dlem  15791  odd2np1  16365  divalgb  16428  gcdcllem2  16524  mrcidb2  17635  fncnvimaeqv  18137  qusecsub  19821  domnmuln0  20674  acsfn1p  20764  lbsacsbs  21122  islpir2  21296  islinds2  21778  islbs4  21797  mplcoe1  22000  mplcoe5  22003  mamucl  22344  mavmulcl  22490  mdetunilem8  22562  iscld4  23008  isconn2  23357  kgencn  23499  tx1cn  23552  tx2cn  23553  elmptrab  23770  isfbas  23772  fbfinnfr  23784  cnfcf  23985  fmucndlem  24234  prdsxmslem2  24473  blval2  24506  cnbl0  24717  cnblcld  24718  metcld  25263  ismbf  25586  ismbfcn  25587  itg1val2  25642  itg2split  25707  itg2monolem1  25708  aannenlem1  26293  pilem1  26418  sinq34lt0t  26475  ellogrn  26525  logeftb  26549  gausslemma2dlem1a  27333  elznns  28347  readdscl  28407  ercgrg  28501  elntg2  28969  usgredgffibi  29308  vtxd0nedgb  29473  vdiscusgrb  29515  upgrspthswlk  29725  s3wwlks2on  29943  clwwlknonwwlknonb  30092  frgrncvvdeqlem2  30286  ch0pss  31431  h1de2ctlem  31541  adjsym  31819  eigposi  31822  dfadj2  31871  elnlfn  31914  xppreima  32628  1stpreima  32689  2ndpreima  32690  creq0  32718  hashgt1  32792  isunit3  33241  isdrng4  33294  qusxpid  33383  lindflbs  33399  dvdsruassoi  33404  dvdsruasso  33405  dvdsrspss  33407  unitprodclb  33409  lsmsnorb  33411  nsgqusf1olem3  33435  qsfld  33518  qtophaus  33872  prsdm  33950  prsrn  33951  1stmbfm  34297  2ndmbfm  34298  eulerpartlemn  34418  reprdifc  34664  circlemeth  34677  bnj1454  34878  bnj984  34988  dffun10  35937  hfext  36206  isfne4b  36364  neifg  36394  taupilem3  37342  topdifinfindis  37369  topdifinffinlem  37370  finxpsuclem  37420  nlpineqsn  37431  wl-ifp-ncond1  37487  poimirlem23  37672  poimirlem26  37675  cnambfre  37697  0totbnd  37802  suceqsneq  38260  opelvvdif  38282  inecmo  38378  brxrn  38397  brin2  38432  eleccossin  38506  dffunsALTV2  38707  dffunsALTV3  38708  dffunsALTV4  38709  elfunsALTV2  38716  elfunsALTV3  38717  elfunsALTV4  38718  elfunsALTV5  38719  dfdisjs2  38732  eldisjs2  38746  disjres  38767  cvrval2  39297  cvrnbtwn2  39298  cvrnbtwn4  39302  hlateq  39423  islpln5  39559  islvol5  39603  pmap11  39786  4atex  40100  cdleme0ex2N  40248  cdlemefrs29pre00  40419  diaord  41071  dihmeetlem13N  41343  lcfl1  41516  lcfls1N  41559  mapdpglem3  41699  isnacs2  42704  mrefg3  42706  pw2f1ocnv  43036  unielss  43217  onmaxnelsup  43222  onsupnmax  43227  onov0suclim  43273  cantnf2  43324  ordsssucb  43334  relexp0eq  43700  frege124d  43760  uneqsn  44024  k0004lem1  44146  sbcoreleleq  44535  modelac8prim  44992  r19.28zf  45163  climreeq  45622  funressnfv  47052  fmtnorec2lem  47536  sclnbgrelself  47841  gpgiedgdmel  48033  gpgedgel  48034  eenglngeehlnmlem1  48697  eenglngeehlnmlem2  48698  rrx2linest2  48704  itsclinecirc0b  48734  map0cor  48813  ipolublem  48940  ipoglblem  48943  functermc  49373