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  535  cad1  1620  necon2abid  2985  reueubd  3357  reu8  3663  sbc6gOLD  3742  r19.28z  4425  r19.37zv  4429  r19.45zv  4430  r19.44zv  4431  r19.27z  4432  r19.36zv  4434  ralidmOLD  4443  ralsnsg  4601  eldifvsn  4727  ssunsn2  4757  iunconst  4930  iinconst  4931  iuneqconst  4932  relsng  5700  opelres  5886  ordsseleq  6280  ordequn  6351  funssres  6462  fncnv  6491  ffrnbd  6600  fresaun  6629  dff1o5  6709  funimass4  6816  fndmdifeq0  6903  fneqeql2  6906  unpreima  6922  dffo3  6960  fnnfpeq0  7032  funfvima  7088  f1eqcocnv  7153  f1eqcocnvOLD  7154  fliftf  7166  isocnv3  7183  isomin  7188  eloprabga  7360  eloprabgaOLD  7361  mpo2eqb  7384  elpwun  7597  dfom2  7689  opabex3d  7781  opabex3rd  7782  opabex3  7783  f1oweALT  7788  fnwelem  7943  mptsuppd  7974  dfrecs3  8174  dfrecs3OLD  8175  oe0m1  8313  oarec  8355  boxcutc  8687  ordunifi  8994  r1fin  9462  rankr1c  9510  iscard  9664  iscard2  9665  cardval2  9680  dfac3  9808  kmlem8  9844  infinf  10253  xrlenlt  10971  ltxrlt  10976  negcon2  11204  mulne0b  11546  dfinfre  11886  crne0  11896  elznn  12265  zmax  12614  elfznelfzo  13420  modmuladdnn0  13563  hashneq0  14007  xpcogend  14613  sqrtneglem  14906  rexfiuz  14987  rexanuz2  14989  sumsplit  15408  fsum2dlem  15410  odd2np1  15978  divalgb  16041  gcdcllem2  16135  mrcidb2  17244  fncnvimaeqv  17752  acsfn1p  19982  lbsacsbs  20333  islpir2  20435  domnmuln0  20482  islinds2  20930  islbs4  20949  mplcoe1  21148  mplcoe5  21151  mamucl  21458  mavmulcl  21604  mdetunilem8  21676  iscld4  22124  isconn2  22473  kgencn  22615  tx1cn  22668  tx2cn  22669  elmptrab  22886  isfbas  22888  fbfinnfr  22900  cnfcf  23101  fmucndlem  23351  prdsxmslem2  23591  blval2  23624  cnbl0  23843  cnblcld  23844  metcld  24375  ismbf  24697  ismbfcn  24698  itg1val2  24753  itg2split  24819  itg2monolem1  24820  aannenlem1  25393  pilem1  25515  sinq34lt0t  25571  ellogrn  25620  logeftb  25644  gausslemma2dlem1a  26418  ercgrg  26782  elntg2  27256  usgredgffibi  27594  vtxd0nedgb  27758  vdiscusgrb  27800  upgrspthswlk  28007  s3wwlks2on  28222  clwwlknonwwlknonb  28371  frgrncvvdeqlem2  28565  ch0pss  29708  h1de2ctlem  29818  adjsym  30096  eigposi  30099  dfadj2  30148  elnlfn  30191  xppreima  30884  1stpreima  30941  2ndpreima  30942  creq0  30972  hashgt1  31030  qusxpid  31461  lindflbs  31476  lsmsnorb  31481  nsgqusf1olem3  31502  qtophaus  31688  prsdm  31766  prsrn  31767  1stmbfm  32127  2ndmbfm  32128  eulerpartlemn  32248  reprdifc  32507  circlemeth  32520  bnj1454  32722  bnj984  32832  eldifsucnn  33597  ttrclselem2  33712  xpord3pred  33725  dffun10  34143  hfext  34412  isfne4b  34457  neifg  34487  taupilem3  35417  topdifinfindis  35444  topdifinffinlem  35445  finxpsuclem  35495  nlpineqsn  35506  wl-ifp-ncond1  35562  poimirlem23  35727  poimirlem26  35730  cnambfre  35752  0totbnd  35858  opelvvdif  36325  inecmo  36414  brxrn  36431  brin2  36462  eleccossin  36528  dffunsALTV2  36722  dffunsALTV3  36723  dffunsALTV4  36724  elfunsALTV2  36731  elfunsALTV3  36732  elfunsALTV4  36733  elfunsALTV5  36734  dfdisjs2  36747  eldisjs2  36761  cvrval2  37215  cvrnbtwn2  37216  cvrnbtwn4  37220  hlateq  37340  islpln5  37476  islvol5  37520  pmap11  37703  4atex  38017  cdleme0ex2N  38165  cdlemefrs29pre00  38336  diaord  38988  dihmeetlem13N  39260  lcfl1  39433  lcfls1N  39476  mapdpglem3  39616  isnacs2  40444  mrefg3  40446  pw2f1ocnv  40775  relexp0eq  41198  frege124d  41258  uneqsn  41522  k0004lem1  41646  sbcoreleleq  42044  dffo3f  42606  climreeq  43044  funressnfv  44424  fmtnorec2lem  44882  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2linest2  45978  itsclinecirc0b  46008  map0cor  46070  ipolublem  46160  ipoglblem  46163