Theorem bitr4id 291

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 225	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 289	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  baib  540  cad1  1624  necon2abid  2976  reueubd  3361  issetft  3447  reu8  3674  r19.28z  4431  r19.37zv  4436  r19.45zv  4437  r19.44zv  4438  r19.27z  4439  r19.36zv  4441  ralsnsg  4603  eldifvsn  4731  ssunsn2  4759  iunconst  4932  iinconst  4933  iuneqconst  4934  relsng  5745  dmxp  5872  opelres  5938  ordsseleq  6340  ordequn  6416  funssres  6530  fncnv  6559  ffrnbd  6671  fresaun  6699  dff1o5  6777  tz6.12c  6850  funimass4  6892  fndmdifeq0  6986  fneqeql2  6989  unpreima  7005  dffo3  7044  dffo3f  7048  fnnfpeq0  7123  funfvima  7175  f1eqcocnv  7246  fliftf  7260  isocnv3  7277  isomin  7282  eloprabga  7466  mpo2eqb  7489  elpwun  7713  dfom2  7809  opabex3d  7908  opabex3rd  7909  opabex3  7910  f1oweALT  7915  fnwelem  8072  mptsuppd  8128  dfrecs3  8303  oe0m1  8447  oarec  8488  eldifsucnn  8591  naddsuc2  8628  boxcutc  8880  ordunifi  9191  ttrclselem2  9639  r1fin  9689  rankr1c  9737  iscard  9891  iscard2  9892  cardval2  9907  dfac3  10035  kmlem8  10072  xrlenlt  11202  ltxrlt  11208  negcon2  11439  mulne0b  11783  dfinfre  12129  crne0  12144  elznn  12532  zmax  12887  elfznelfzo  13720  modmuladdnn0  13869  hashneq0  14318  xpcogend  14928  sqrtneglem  15220  rexfiuz  15302  rexanuz2  15304  sumsplit  15722  fsum2dlem  15724  odd2np1  16302  divalgb  16365  gcdcllem2  16461  mrcidb2  17576  fncnvimaeqv  18078  qusecsub  19802  domnmuln0  20682  acsfn1p  20772  lbsacsbs  21150  islpir2  21324  islinds2  21789  islbs4  21808  mplcoe1  22014  mplcoe5  22017  mamucl  22385  mavmulcl  22531  mdetunilem8  22603  iscld4  23049  isconn2  23398  kgencn  23540  tx1cn  23593  tx2cn  23594  elmptrab  23811  isfbas  23813  fbfinnfr  23825  cnfcf  24026  fmucndlem  24274  prdsxmslem2  24513  blval2  24546  cnbl0  24757  cnblcld  24758  metcld  25292  ismbf  25614  ismbfcn  25615  itg1val2  25670  itg2split  25735  itg2monolem1  25736  aannenlem1  26313  pilem1  26435  sinq34lt0t  26492  ellogrn  26542  logeftb  26566  gausslemma2dlem1a  27347  sltssnb  27780  bdayle  27927  elznns  28413  zsoring  28420  readdscl  28510  ercgrg  28604  elntg2  29073  usgredgffibi  29412  vtxd0nedgb  29576  vdiscusgrb  29618  upgrspthswlk  29825  s3wwlks2on  30043  sps3wwlks2on  30044  clwwlknonwwlknonb  30195  frgrncvvdeqlem2  30389  ch0pss  31535  h1de2ctlem  31645  adjsym  31923  eigposi  31926  dfadj2  31975  elnlfn  32018  xppreima  32738  1stpreima  32800  2ndpreima  32801  creq0  32829  hashgt1  32901  isunit3  33323  isdrng4  33380  qusxpid  33447  lindflbs  33463  dvdsruassoi  33468  dvdsruasso  33469  dvdsrspss  33471  unitprodclb  33473  lsmsnorb  33475  nsgqusf1olem3  33499  qsfld  33582  esplyind  33768  qtophaus  34029  prsdm  34107  prsrn  34108  1stmbfm  34453  2ndmbfm  34454  eulerpartlemn  34574  reprdifc  34820  circlemeth  34833  bnj1454  35033  bnj984  35143  vonf1owev  35345  dffun10  36149  hfext  36420  isfne4b  36578  neifg  36608  taupilem3  37688  topdifinfindis  37717  topdifinffinlem  37718  finxpsuclem  37768  nlpineqsn  37779  wl-ifp-ncond1  37835  poimirlem23  38019  poimirlem26  38022  cnambfre  38044  0totbnd  38149  opelvvdif  38640  inecmo  38731  brxrn  38759  brin2  38814  suceqsneq  38860  eleccossin  38949  dffunsALTV2  39145  dffunsALTV3  39146  dffunsALTV4  39147  elfunsALTV2  39154  elfunsALTV3  39155  elfunsALTV4  39156  elfunsALTV5  39157  dfdisjs2  39170  eldisjs2  39196  disjres  39220  cvrval2  39775  cvrnbtwn2  39776  cvrnbtwn4  39780  hlateq  39900  islpln5  40036  islvol5  40080  pmap11  40263  4atex  40577  cdleme0ex2N  40725  cdlemefrs29pre00  40896  diaord  41548  dihmeetlem13N  41820  lcfl1  41993  lcfls1N  42036  mapdpglem3  42176  isnacs2  43164  mrefg3  43166  pw2f1ocnv  43491  unielss  43672  onmaxnelsup  43677  onsupnmax  43682  onov0suclim  43728  cantnf2  43779  ordsssucb  43789  relexp0eq  44154  frege124d  44214  uneqsn  44478  k0004lem1  44600  sbcoreleleq  44988  modelac8prim  45445  r19.28zf  45614  climreeq  46066  funressnfv  47514  2timesltsqm1  47850  fmtnorec2lem  48028  sclnbgrelself  48347  gpgiedgdmel  48548  gpgedgel  48549  eenglngeehlnmlem1  49236  eenglngeehlnmlem2  49237  rrx2linest2  49243  itsclinecirc0b  49273  map0cor  49353  ipolublem  49484  ipoglblem  49487  functermc  50006