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  2967  reueubd  3362  issetft  3452  reu8  3693  r19.28z  4449  r19.37zv  4453  r19.45zv  4454  r19.44zv  4455  r19.27z  4456  r19.36zv  4458  ralsnsg  4622  eldifvsn  4748  ssunsn2  4778  iunconst  4951  iinconst  4952  iuneqconst  4953  relsng  5744  dmxp  5871  opelres  5936  ordsseleq  6336  ordequn  6412  funssres  6526  fncnv  6555  ffrnbd  6667  fresaun  6695  dff1o5  6773  tz6.12c  6844  funimass4  6887  fndmdifeq0  6978  fneqeql2  6981  unpreima  6997  dffo3  7036  dffo3f  7040  fnnfpeq0  7114  funfvima  7166  f1eqcocnv  7238  fliftf  7252  isocnv3  7269  isomin  7274  eloprabga  7458  mpo2eqb  7481  elpwun  7705  dfom2  7801  opabex3d  7900  opabex3rd  7901  opabex3  7902  f1oweALT  7907  fnwelem  8064  mptsuppd  8120  dfrecs3  8295  oe0m1  8439  oarec  8480  eldifsucnn  8582  naddsuc2  8619  boxcutc  8868  ordunifi  9179  ttrclselem2  9622  r1fin  9669  rankr1c  9717  iscard  9871  iscard2  9872  cardval2  9887  dfac3  10015  kmlem8  10052  infinf  10460  xrlenlt  11180  ltxrlt  11186  negcon2  11417  mulne0b  11761  dfinfre  12106  crne0  12121  elznn  12487  zmax  12846  elfznelfzo  13675  modmuladdnn0  13822  hashneq0  14271  xpcogend  14881  sqrtneglem  15173  rexfiuz  15255  rexanuz2  15257  sumsplit  15675  fsum2dlem  15677  odd2np1  16252  divalgb  16315  gcdcllem2  16411  mrcidb2  17524  fncnvimaeqv  18026  qusecsub  19714  domnmuln0  20594  acsfn1p  20684  lbsacsbs  21063  islpir2  21237  islinds2  21720  islbs4  21739  mplcoe1  21942  mplcoe5  21945  mamucl  22286  mavmulcl  22432  mdetunilem8  22504  iscld4  22950  isconn2  23299  kgencn  23441  tx1cn  23494  tx2cn  23495  elmptrab  23712  isfbas  23714  fbfinnfr  23726  cnfcf  23927  fmucndlem  24176  prdsxmslem2  24415  blval2  24448  cnbl0  24659  cnblcld  24660  metcld  25204  ismbf  25527  ismbfcn  25528  itg1val2  25583  itg2split  25648  itg2monolem1  25649  aannenlem1  26234  pilem1  26359  sinq34lt0t  26416  ellogrn  26466  logeftb  26490  gausslemma2dlem1a  27274  bdayle  27830  elznns  28295  zsoring  28301  readdscl  28368  ercgrg  28462  elntg2  28930  usgredgffibi  29269  vtxd0nedgb  29434  vdiscusgrb  29476  upgrspthswlk  29683  s3wwlks2on  29901  clwwlknonwwlknonb  30050  frgrncvvdeqlem2  30244  ch0pss  31389  h1de2ctlem  31499  adjsym  31777  eigposi  31780  dfadj2  31829  elnlfn  31872  xppreima  32589  1stpreima  32650  2ndpreima  32651  creq0  32680  hashgt1  32754  isunit3  33182  isdrng4  33235  qusxpid  33301  lindflbs  33317  dvdsruassoi  33322  dvdsruasso  33323  dvdsrspss  33325  unitprodclb  33327  lsmsnorb  33329  nsgqusf1olem3  33353  qsfld  33436  qtophaus  33809  prsdm  33887  prsrn  33888  1stmbfm  34234  2ndmbfm  34235  eulerpartlemn  34355  reprdifc  34601  circlemeth  34614  bnj1454  34815  bnj984  34925  vonf1owev  35091  dffun10  35898  hfext  36167  isfne4b  36325  neifg  36355  taupilem3  37303  topdifinfindis  37330  topdifinffinlem  37331  finxpsuclem  37381  nlpineqsn  37392  wl-ifp-ncond1  37448  poimirlem23  37633  poimirlem26  37636  cnambfre  37658  0totbnd  37763  suceqsneq  38221  opelvvdif  38244  inecmo  38333  brxrn  38352  brin2  38396  eleccossin  38470  dffunsALTV2  38672  dffunsALTV3  38673  dffunsALTV4  38674  elfunsALTV2  38681  elfunsALTV3  38682  elfunsALTV4  38683  elfunsALTV5  38684  dfdisjs2  38697  eldisjs2  38711  disjres  38732  cvrval2  39263  cvrnbtwn2  39264  cvrnbtwn4  39268  hlateq  39388  islpln5  39524  islvol5  39568  pmap11  39751  4atex  40065  cdleme0ex2N  40213  cdlemefrs29pre00  40384  diaord  41036  dihmeetlem13N  41308  lcfl1  41481  lcfls1N  41524  mapdpglem3  41664  isnacs2  42689  mrefg3  42691  pw2f1ocnv  43020  unielss  43201  onmaxnelsup  43206  onsupnmax  43211  onov0suclim  43257  cantnf2  43308  ordsssucb  43318  relexp0eq  43684  frege124d  43744  uneqsn  44008  k0004lem1  44130  sbcoreleleq  44519  modelac8prim  44976  r19.28zf  45147  climreeq  45604  funressnfv  47037  fmtnorec2lem  47536  sclnbgrelself  47842  gpgiedgdmel  48043  gpgedgel  48044  eenglngeehlnmlem1  48732  eenglngeehlnmlem2  48733  rrx2linest2  48739  itsclinecirc0b  48769  map0cor  48849  ipolublem  48980  ipoglblem  48983  functermc  49503