Theorem bitr4id 289

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  baib  536  cad1  1618  necon2abid  2983  reueubd  3395  reu8  3729  sbc6gOLD  3808  r19.28z  4497  r19.37zv  4501  r19.45zv  4502  r19.44zv  4503  r19.27z  4504  r19.36zv  4506  ralidmOLD  4515  ralsnsg  4672  eldifvsn  4800  ssunsn2  4830  iunconst  5006  iinconst  5007  iuneqconst  5008  relsng  5801  opelres  5987  ordsseleq  6393  ordequn  6467  funssres  6592  fncnv  6621  ffrnbd  6733  fresaun  6762  dff1o5  6842  tz6.12c  6913  funimass4  6956  fndmdifeq0  7045  fneqeql2  7048  unpreima  7064  dffo3  7103  dffo3f  7107  fnnfpeq0  7178  funfvima  7234  f1eqcocnv  7301  f1eqcocnvOLD  7302  fliftf  7314  isocnv3  7331  isomin  7336  eloprabga  7518  eloprabgaOLD  7519  mpo2eqb  7543  elpwun  7758  dfom2  7859  opabex3d  7954  opabex3rd  7955  opabex3  7956  f1oweALT  7961  fnwelem  8119  mptsuppd  8174  dfrecs3  8374  dfrecs3OLD  8375  oe0m1  8523  oarec  8564  eldifsucnn  8665  boxcutc  8937  ordunifi  9295  ttrclselem2  9723  r1fin  9770  rankr1c  9818  iscard  9972  iscard2  9973  cardval2  9988  dfac3  10118  kmlem8  10154  infinf  10563  xrlenlt  11283  ltxrlt  11288  negcon2  11517  mulne0b  11859  dfinfre  12199  crne0  12209  elznn  12578  zmax  12933  elfznelfzo  13741  modmuladdnn0  13884  hashneq0  14328  xpcogend  14925  sqrtneglem  15217  rexfiuz  15298  rexanuz2  15300  sumsplit  15718  fsum2dlem  15720  odd2np1  16288  divalgb  16351  gcdcllem2  16445  mrcidb2  17566  fncnvimaeqv  18075  qusecsub  19744  acsfn1p  20558  lbsacsbs  20914  islpir2  21089  domnmuln0  21114  islinds2  21587  islbs4  21606  mplcoe1  21811  mplcoe5  21814  mamucl  22121  mavmulcl  22269  mdetunilem8  22341  iscld4  22789  isconn2  23138  kgencn  23280  tx1cn  23333  tx2cn  23334  elmptrab  23551  isfbas  23553  fbfinnfr  23565  cnfcf  23766  fmucndlem  24016  prdsxmslem2  24258  blval2  24291  cnbl0  24510  cnblcld  24511  metcld  25047  ismbf  25369  ismbfcn  25370  itg1val2  25425  itg2split  25491  itg2monolem1  25492  aannenlem1  26065  pilem1  26187  sinq34lt0t  26243  ellogrn  26292  logeftb  26316  gausslemma2dlem1a  27092  ercgrg  28023  elntg2  28498  usgredgffibi  28836  vtxd0nedgb  29000  vdiscusgrb  29042  upgrspthswlk  29250  s3wwlks2on  29465  clwwlknonwwlknonb  29614  frgrncvvdeqlem2  29808  ch0pss  30953  h1de2ctlem  31063  adjsym  31341  eigposi  31344  dfadj2  31393  elnlfn  31436  xppreima  32126  1stpreima  32183  2ndpreima  32184  creq0  32215  hashgt1  32275  isdrng4  32653  qusxpid  32737  dvdsruassoi  32751  dvdsruasso  32752  dvdsrspss  32753  lindflbs  32757  lsmsnorb  32763  nsgqusf1olem3  32788  qsfld  32874  qtophaus  33102  prsdm  33180  prsrn  33181  1stmbfm  33545  2ndmbfm  33546  eulerpartlemn  33666  reprdifc  33925  circlemeth  33938  bnj1454  34139  bnj984  34249  dffun10  35178  hfext  35447  isfne4b  35529  neifg  35559  taupilem3  36503  topdifinfindis  36530  topdifinffinlem  36531  finxpsuclem  36581  nlpineqsn  36592  wl-ifp-ncond1  36648  poimirlem23  36814  poimirlem26  36817  cnambfre  36839  0totbnd  36944  suceqsneq  37406  opelvvdif  37430  inecmo  37527  brxrn  37547  brin2  37582  eleccossin  37656  dffunsALTV2  37857  dffunsALTV3  37858  dffunsALTV4  37859  elfunsALTV2  37866  elfunsALTV3  37867  elfunsALTV4  37868  elfunsALTV5  37869  dfdisjs2  37882  eldisjs2  37896  disjres  37917  cvrval2  38447  cvrnbtwn2  38448  cvrnbtwn4  38452  hlateq  38573  islpln5  38709  islvol5  38753  pmap11  38936  4atex  39250  cdleme0ex2N  39398  cdlemefrs29pre00  39569  diaord  40221  dihmeetlem13N  40493  lcfl1  40666  lcfls1N  40709  mapdpglem3  40849  isnacs2  41746  mrefg3  41748  pw2f1ocnv  42078  unielss  42269  onmaxnelsup  42274  onsupnmax  42279  onov0suclim  42326  cantnf2  42377  ordsssucb  42387  naddsuc2  42445  relexp0eq  42754  frege124d  42814  uneqsn  43078  k0004lem1  43200  sbcoreleleq  43598  r19.28zf  44155  climreeq  44628  funressnfv  46052  fmtnorec2lem  46509  eenglngeehlnmlem1  47511  eenglngeehlnmlem2  47512  rrx2linest2  47518  itsclinecirc0b  47548  map0cor  47609  ipolublem  47699  ipoglblem  47702