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  1618  necon2abid  2972  reueubd  3365  issetft  3454  reu8  3689  r19.28z  4453  r19.37zv  4458  r19.45zv  4459  r19.44zv  4460  r19.27z  4461  r19.36zv  4463  ralsnsg  4625  eldifvsn  4751  ssunsn2  4781  iunconst  4954  iinconst  4955  iuneqconst  4956  relsng  5748  dmxp  5876  opelres  5942  ordsseleq  6344  ordequn  6420  funssres  6534  fncnv  6563  ffrnbd  6675  fresaun  6703  dff1o5  6781  tz6.12c  6854  funimass4  6896  fndmdifeq0  6987  fneqeql2  6990  unpreima  7006  dffo3  7045  dffo3f  7049  fnnfpeq0  7122  funfvima  7174  f1eqcocnv  7245  fliftf  7259  isocnv3  7276  isomin  7281  eloprabga  7465  mpo2eqb  7488  elpwun  7712  dfom2  7808  opabex3d  7907  opabex3rd  7908  opabex3  7909  f1oweALT  7914  fnwelem  8071  mptsuppd  8127  dfrecs3  8302  oe0m1  8446  oarec  8487  eldifsucnn  8590  naddsuc2  8627  boxcutc  8877  ordunifi  9188  ttrclselem2  9633  r1fin  9683  rankr1c  9731  iscard  9885  iscard2  9886  cardval2  9901  dfac3  10029  kmlem8  10066  xrlenlt  11195  ltxrlt  11201  negcon2  11432  mulne0b  11776  dfinfre  12121  crne0  12136  elznn  12502  zmax  12856  elfznelfzo  13687  modmuladdnn0  13836  hashneq0  14285  xpcogend  14895  sqrtneglem  15187  rexfiuz  15269  rexanuz2  15271  sumsplit  15689  fsum2dlem  15691  odd2np1  16266  divalgb  16329  gcdcllem2  16425  mrcidb2  17539  fncnvimaeqv  18041  qusecsub  19762  domnmuln0  20640  acsfn1p  20730  lbsacsbs  21109  islpir2  21283  islinds2  21766  islbs4  21785  mplcoe1  21990  mplcoe5  21993  mamucl  22343  mavmulcl  22489  mdetunilem8  22561  iscld4  23007  isconn2  23356  kgencn  23498  tx1cn  23551  tx2cn  23552  elmptrab  23769  isfbas  23771  fbfinnfr  23783  cnfcf  23984  fmucndlem  24232  prdsxmslem2  24471  blval2  24504  cnbl0  24715  cnblcld  24716  metcld  25260  ismbf  25583  ismbfcn  25584  itg1val2  25639  itg2split  25704  itg2monolem1  25705  aannenlem1  26290  pilem1  26415  sinq34lt0t  26472  ellogrn  26522  logeftb  26546  gausslemma2dlem1a  27330  ssltsnb  27759  bdayle  27888  elznns  28360  zsoring  28367  readdscl  28444  ercgrg  28538  elntg2  29007  usgredgffibi  29346  vtxd0nedgb  29511  vdiscusgrb  29553  upgrspthswlk  29760  s3wwlks2on  29978  sps3wwlks2on  29979  clwwlknonwwlknonb  30130  frgrncvvdeqlem2  30324  ch0pss  31469  h1de2ctlem  31579  adjsym  31857  eigposi  31860  dfadj2  31909  elnlfn  31952  xppreima  32672  1stpreima  32735  2ndpreima  32736  creq0  32764  hashgt1  32837  isunit3  33272  isdrng4  33326  qusxpid  33393  lindflbs  33409  dvdsruassoi  33414  dvdsruasso  33415  dvdsrspss  33417  unitprodclb  33419  lsmsnorb  33421  nsgqusf1olem3  33445  qsfld  33528  esplyind  33680  qtophaus  33942  prsdm  34020  prsrn  34021  1stmbfm  34366  2ndmbfm  34367  eulerpartlemn  34487  reprdifc  34733  circlemeth  34746  bnj1454  34947  bnj984  35057  vonf1owev  35251  dffun10  36055  hfext  36326  isfne4b  36484  neifg  36514  taupilem3  37463  topdifinfindis  37490  topdifinffinlem  37491  finxpsuclem  37541  nlpineqsn  37552  wl-ifp-ncond1  37608  poimirlem23  37783  poimirlem26  37786  cnambfre  37808  0totbnd  37913  opelvvdif  38396  inecmo  38487  brxrn  38507  brin2  38562  suceqsneq  38596  eleccossin  38685  dffunsALTV2  38882  dffunsALTV3  38883  dffunsALTV4  38884  elfunsALTV2  38891  elfunsALTV3  38892  elfunsALTV4  38893  elfunsALTV5  38894  dfdisjs2  38907  eldisjs2  38921  disjres  38942  cvrval2  39473  cvrnbtwn2  39474  cvrnbtwn4  39478  hlateq  39598  islpln5  39734  islvol5  39778  pmap11  39961  4atex  40275  cdleme0ex2N  40423  cdlemefrs29pre00  40594  diaord  41246  dihmeetlem13N  41518  lcfl1  41691  lcfls1N  41734  mapdpglem3  41874  isnacs2  42890  mrefg3  42892  pw2f1ocnv  43221  unielss  43402  onmaxnelsup  43407  onsupnmax  43412  onov0suclim  43458  cantnf2  43509  ordsssucb  43519  relexp0eq  43884  frege124d  43944  uneqsn  44208  k0004lem1  44330  sbcoreleleq  44718  modelac8prim  45175  r19.28zf  45345  climreeq  45801  funressnfv  47231  fmtnorec2lem  47730  sclnbgrelself  48036  gpgiedgdmel  48237  gpgedgel  48238  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2linest2  48932  itsclinecirc0b  48962  map0cor  49042  ipolublem  49173  ipoglblem  49176  functermc  49695