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  2968  reueubd  3375  issetft  3466  reu8  3706  r19.28z  4463  r19.37zv  4467  r19.45zv  4468  r19.44zv  4469  r19.27z  4470  r19.36zv  4472  ralsnsg  4636  eldifvsn  4763  ssunsn2  4793  iunconst  4967  iinconst  4968  iuneqconst  4969  relsng  5766  dmxp  5894  opelres  5958  ordsseleq  6363  ordequn  6439  funssres  6562  fncnv  6591  ffrnbd  6705  fresaun  6733  dff1o5  6811  tz6.12c  6882  funimass4  6927  fndmdifeq0  7018  fneqeql2  7021  unpreima  7037  dffo3  7076  dffo3f  7080  fnnfpeq0  7154  funfvima  7206  f1eqcocnv  7278  fliftf  7292  isocnv3  7309  isomin  7314  eloprabga  7500  mpo2eqb  7523  elpwun  7747  dfom2  7846  opabex3d  7946  opabex3rd  7947  opabex3  7948  f1oweALT  7953  fnwelem  8112  mptsuppd  8168  dfrecs3  8343  oe0m1  8487  oarec  8528  eldifsucnn  8630  naddsuc2  8667  boxcutc  8916  ordunifi  9243  ttrclselem2  9685  r1fin  9732  rankr1c  9780  iscard  9934  iscard2  9935  cardval2  9950  dfac3  10080  kmlem8  10117  infinf  10525  xrlenlt  11245  ltxrlt  11250  negcon2  11481  mulne0b  11825  dfinfre  12170  crne0  12180  elznn  12551  zmax  12910  elfznelfzo  13739  modmuladdnn0  13886  hashneq0  14335  xpcogend  14946  sqrtneglem  15238  rexfiuz  15320  rexanuz2  15322  sumsplit  15740  fsum2dlem  15742  odd2np1  16317  divalgb  16380  gcdcllem2  16476  mrcidb2  17585  fncnvimaeqv  18087  qusecsub  19771  domnmuln0  20624  acsfn1p  20714  lbsacsbs  21072  islpir2  21246  islinds2  21728  islbs4  21747  mplcoe1  21950  mplcoe5  21953  mamucl  22294  mavmulcl  22440  mdetunilem8  22512  iscld4  22958  isconn2  23307  kgencn  23449  tx1cn  23502  tx2cn  23503  elmptrab  23720  isfbas  23722  fbfinnfr  23734  cnfcf  23935  fmucndlem  24184  prdsxmslem2  24423  blval2  24456  cnbl0  24667  cnblcld  24668  metcld  25212  ismbf  25535  ismbfcn  25536  itg1val2  25591  itg2split  25656  itg2monolem1  25657  aannenlem1  26242  pilem1  26367  sinq34lt0t  26424  ellogrn  26474  logeftb  26498  gausslemma2dlem1a  27282  elznns  28296  readdscl  28356  ercgrg  28450  elntg2  28918  usgredgffibi  29257  vtxd0nedgb  29422  vdiscusgrb  29464  upgrspthswlk  29674  s3wwlks2on  29892  clwwlknonwwlknonb  30041  frgrncvvdeqlem2  30235  ch0pss  31380  h1de2ctlem  31490  adjsym  31768  eigposi  31771  dfadj2  31820  elnlfn  31863  xppreima  32575  1stpreima  32636  2ndpreima  32637  creq0  32665  hashgt1  32739  isunit3  33198  isdrng4  33251  qusxpid  33340  lindflbs  33356  dvdsruassoi  33361  dvdsruasso  33362  dvdsrspss  33364  unitprodclb  33366  lsmsnorb  33368  nsgqusf1olem3  33392  qsfld  33475  qtophaus  33832  prsdm  33910  prsrn  33911  1stmbfm  34257  2ndmbfm  34258  eulerpartlemn  34378  reprdifc  34624  circlemeth  34637  bnj1454  34838  bnj984  34948  dffun10  35897  hfext  36166  isfne4b  36324  neifg  36354  taupilem3  37302  topdifinfindis  37329  topdifinffinlem  37330  finxpsuclem  37380  nlpineqsn  37391  wl-ifp-ncond1  37447  poimirlem23  37632  poimirlem26  37635  cnambfre  37657  0totbnd  37762  suceqsneq  38220  opelvvdif  38243  inecmo  38332  brxrn  38351  brin2  38395  eleccossin  38469  dffunsALTV2  38671  dffunsALTV3  38672  dffunsALTV4  38673  elfunsALTV2  38680  elfunsALTV3  38681  elfunsALTV4  38682  elfunsALTV5  38683  dfdisjs2  38696  eldisjs2  38710  disjres  38731  cvrval2  39262  cvrnbtwn2  39263  cvrnbtwn4  39267  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  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  47034  fmtnorec2lem  47533  sclnbgrelself  47838  gpgiedgdmel  48030  gpgedgel  48031  eenglngeehlnmlem1  48716  eenglngeehlnmlem2  48717  rrx2linest2  48723  itsclinecirc0b  48753  map0cor  48833  ipolublem  48964  ipoglblem  48967  functermc  49487