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  3370  issetft  3460  reu8  3701  r19.28z  4457  r19.37zv  4461  r19.45zv  4462  r19.44zv  4463  r19.27z  4464  r19.36zv  4466  ralsnsg  4630  eldifvsn  4757  ssunsn2  4787  iunconst  4961  iinconst  4962  iuneqconst  4963  relsng  5755  dmxp  5882  opelres  5945  ordsseleq  6349  ordequn  6425  funssres  6544  fncnv  6573  ffrnbd  6685  fresaun  6713  dff1o5  6791  tz6.12c  6862  funimass4  6907  fndmdifeq0  6998  fneqeql2  7001  unpreima  7017  dffo3  7056  dffo3f  7060  fnnfpeq0  7134  funfvima  7186  f1eqcocnv  7258  fliftf  7272  isocnv3  7289  isomin  7294  eloprabga  7478  mpo2eqb  7501  elpwun  7725  dfom2  7824  opabex3d  7923  opabex3rd  7924  opabex3  7925  f1oweALT  7930  fnwelem  8087  mptsuppd  8143  dfrecs3  8318  oe0m1  8462  oarec  8503  eldifsucnn  8605  naddsuc2  8642  boxcutc  8891  ordunifi  9213  ttrclselem2  9655  r1fin  9702  rankr1c  9750  iscard  9904  iscard2  9905  cardval2  9920  dfac3  10050  kmlem8  10087  infinf  10495  xrlenlt  11215  ltxrlt  11220  negcon2  11451  mulne0b  11795  dfinfre  12140  crne0  12155  elznn  12521  zmax  12880  elfznelfzo  13709  modmuladdnn0  13856  hashneq0  14305  xpcogend  14916  sqrtneglem  15208  rexfiuz  15290  rexanuz2  15292  sumsplit  15710  fsum2dlem  15712  odd2np1  16287  divalgb  16350  gcdcllem2  16446  mrcidb2  17559  fncnvimaeqv  18061  qusecsub  19749  domnmuln0  20629  acsfn1p  20719  lbsacsbs  21098  islpir2  21272  islinds2  21755  islbs4  21774  mplcoe1  21977  mplcoe5  21980  mamucl  22321  mavmulcl  22467  mdetunilem8  22539  iscld4  22985  isconn2  23334  kgencn  23476  tx1cn  23529  tx2cn  23530  elmptrab  23747  isfbas  23749  fbfinnfr  23761  cnfcf  23962  fmucndlem  24211  prdsxmslem2  24450  blval2  24483  cnbl0  24694  cnblcld  24695  metcld  25239  ismbf  25562  ismbfcn  25563  itg1val2  25618  itg2split  25683  itg2monolem1  25684  aannenlem1  26269  pilem1  26394  sinq34lt0t  26451  ellogrn  26501  logeftb  26525  gausslemma2dlem1a  27309  bdayle  27865  elznns  28330  zsoring  28336  readdscl  28403  ercgrg  28497  elntg2  28965  usgredgffibi  29304  vtxd0nedgb  29469  vdiscusgrb  29511  upgrspthswlk  29718  s3wwlks2on  29936  clwwlknonwwlknonb  30085  frgrncvvdeqlem2  30279  ch0pss  31424  h1de2ctlem  31534  adjsym  31812  eigposi  31815  dfadj2  31864  elnlfn  31907  xppreima  32619  1stpreima  32680  2ndpreima  32681  creq0  32709  hashgt1  32783  isunit3  33208  isdrng4  33261  qusxpid  33327  lindflbs  33343  dvdsruassoi  33348  dvdsruasso  33349  dvdsrspss  33351  unitprodclb  33353  lsmsnorb  33355  nsgqusf1olem3  33379  qsfld  33462  qtophaus  33819  prsdm  33897  prsrn  33898  1stmbfm  34244  2ndmbfm  34245  eulerpartlemn  34365  reprdifc  34611  circlemeth  34624  bnj1454  34825  bnj984  34935  vonf1owev  35088  dffun10  35895  hfext  36164  isfne4b  36322  neifg  36352  taupilem3  37300  topdifinfindis  37327  topdifinffinlem  37328  finxpsuclem  37378  nlpineqsn  37389  wl-ifp-ncond1  37445  poimirlem23  37630  poimirlem26  37633  cnambfre  37655  0totbnd  37760  suceqsneq  38218  opelvvdif  38241  inecmo  38330  brxrn  38349  brin2  38393  eleccossin  38467  dffunsALTV2  38669  dffunsALTV3  38670  dffunsALTV4  38671  elfunsALTV2  38678  elfunsALTV3  38679  elfunsALTV4  38680  elfunsALTV5  38681  dfdisjs2  38694  eldisjs2  38708  disjres  38729  cvrval2  39260  cvrnbtwn2  39261  cvrnbtwn4  39265  hlateq  39386  islpln5  39522  islvol5  39566  pmap11  39749  4atex  40063  cdleme0ex2N  40211  cdlemefrs29pre00  40382  diaord  41034  dihmeetlem13N  41306  lcfl1  41479  lcfls1N  41522  mapdpglem3  41662  isnacs2  42687  mrefg3  42689  pw2f1ocnv  43019  unielss  43200  onmaxnelsup  43205  onsupnmax  43210  onov0suclim  43256  cantnf2  43307  ordsssucb  43317  relexp0eq  43683  frege124d  43743  uneqsn  44007  k0004lem1  44129  sbcoreleleq  44518  modelac8prim  44975  r19.28zf  45146  climreeq  45604  funressnfv  47037  fmtnorec2lem  47536  sclnbgrelself  47841  gpgiedgdmel  48033  gpgedgel  48034  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  rrx2linest2  48726  itsclinecirc0b  48756  map0cor  48836  ipolublem  48967  ipoglblem  48970  functermc  49490