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  1619  necon2abid  2975  reueubd  3369  issetft  3458  reu8  3693  r19.28z  4457  r19.37zv  4462  r19.45zv  4463  r19.44zv  4464  r19.27z  4465  r19.36zv  4467  ralsnsg  4629  eldifvsn  4755  ssunsn2  4785  iunconst  4958  iinconst  4959  iuneqconst  4960  relsng  5758  dmxp  5886  opelres  5952  ordsseleq  6354  ordequn  6430  funssres  6544  fncnv  6573  ffrnbd  6685  fresaun  6713  dff1o5  6791  tz6.12c  6864  funimass4  6906  fndmdifeq0  6998  fneqeql2  7001  unpreima  7017  dffo3  7056  dffo3f  7060  fnnfpeq0  7134  funfvima  7186  f1eqcocnv  7257  fliftf  7271  isocnv3  7288  isomin  7293  eloprabga  7477  mpo2eqb  7500  elpwun  7724  dfom2  7820  opabex3d  7919  opabex3rd  7920  opabex3  7921  f1oweALT  7926  fnwelem  8083  mptsuppd  8139  dfrecs3  8314  oe0m1  8458  oarec  8499  eldifsucnn  8602  naddsuc2  8639  boxcutc  8891  ordunifi  9202  ttrclselem2  9647  r1fin  9697  rankr1c  9745  iscard  9899  iscard2  9900  cardval2  9915  dfac3  10043  kmlem8  10080  xrlenlt  11209  ltxrlt  11215  negcon2  11446  mulne0b  11790  dfinfre  12135  crne0  12150  elznn  12516  zmax  12870  elfznelfzo  13701  modmuladdnn0  13850  hashneq0  14299  xpcogend  14909  sqrtneglem  15201  rexfiuz  15283  rexanuz2  15285  sumsplit  15703  fsum2dlem  15705  odd2np1  16280  divalgb  16343  gcdcllem2  16439  mrcidb2  17553  fncnvimaeqv  18055  qusecsub  19779  domnmuln0  20657  acsfn1p  20747  lbsacsbs  21126  islpir2  21300  islinds2  21783  islbs4  21802  mplcoe1  22007  mplcoe5  22010  mamucl  22360  mavmulcl  22506  mdetunilem8  22578  iscld4  23024  isconn2  23373  kgencn  23515  tx1cn  23568  tx2cn  23569  elmptrab  23786  isfbas  23788  fbfinnfr  23800  cnfcf  24001  fmucndlem  24249  prdsxmslem2  24488  blval2  24521  cnbl0  24732  cnblcld  24733  metcld  25277  ismbf  25600  ismbfcn  25601  itg1val2  25656  itg2split  25721  itg2monolem1  25722  aannenlem1  26307  pilem1  26432  sinq34lt0t  26489  ellogrn  26539  logeftb  26563  gausslemma2dlem1a  27347  sltssnb  27780  bdayle  27927  elznns  28413  zsoring  28420  readdscl  28510  ercgrg  28605  elntg2  29074  usgredgffibi  29413  vtxd0nedgb  29578  vdiscusgrb  29620  upgrspthswlk  29827  s3wwlks2on  30045  sps3wwlks2on  30046  clwwlknonwwlknonb  30197  frgrncvvdeqlem2  30391  ch0pss  31537  h1de2ctlem  31647  adjsym  31925  eigposi  31928  dfadj2  31977  elnlfn  32020  xppreima  32739  1stpreima  32801  2ndpreima  32802  creq0  32830  hashgt1  32903  isunit3  33339  isdrng4  33393  qusxpid  33460  lindflbs  33476  dvdsruassoi  33481  dvdsruasso  33482  dvdsrspss  33484  unitprodclb  33486  lsmsnorb  33488  nsgqusf1olem3  33512  qsfld  33595  esplyind  33756  qtophaus  34018  prsdm  34096  prsrn  34097  1stmbfm  34442  2ndmbfm  34443  eulerpartlemn  34563  reprdifc  34809  circlemeth  34822  bnj1454  35022  bnj984  35132  vonf1owev  35328  dffun10  36132  hfext  36403  isfne4b  36561  neifg  36591  taupilem3  37578  topdifinfindis  37605  topdifinffinlem  37606  finxpsuclem  37656  nlpineqsn  37667  wl-ifp-ncond1  37723  poimirlem23  37898  poimirlem26  37901  cnambfre  37923  0totbnd  38028  opelvvdif  38519  inecmo  38610  brxrn  38638  brin2  38693  suceqsneq  38739  eleccossin  38828  dffunsALTV2  39024  dffunsALTV3  39025  dffunsALTV4  39026  elfunsALTV2  39033  elfunsALTV3  39034  elfunsALTV4  39035  elfunsALTV5  39036  dfdisjs2  39049  eldisjs2  39075  disjres  39099  cvrval2  39654  cvrnbtwn2  39655  cvrnbtwn4  39659  hlateq  39779  islpln5  39915  islvol5  39959  pmap11  40142  4atex  40456  cdleme0ex2N  40604  cdlemefrs29pre00  40775  diaord  41427  dihmeetlem13N  41699  lcfl1  41872  lcfls1N  41915  mapdpglem3  42055  isnacs2  43067  mrefg3  43069  pw2f1ocnv  43398  unielss  43579  onmaxnelsup  43584  onsupnmax  43589  onov0suclim  43635  cantnf2  43686  ordsssucb  43696  relexp0eq  44061  frege124d  44121  uneqsn  44385  k0004lem1  44507  sbcoreleleq  44895  modelac8prim  45352  r19.28zf  45522  climreeq  45977  funressnfv  47407  fmtnorec2lem  47906  sclnbgrelself  48212  gpgiedgdmel  48413  gpgedgel  48414  eenglngeehlnmlem1  49101  eenglngeehlnmlem2  49102  rrx2linest2  49108  itsclinecirc0b  49138  map0cor  49218  ipolublem  49349  ipoglblem  49352  functermc  49871