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  1619  necon2abid  2975  reueubd  3360  issetft  3446  reu8  3680  r19.28z  4443  r19.37zv  4448  r19.45zv  4449  r19.44zv  4450  r19.27z  4451  r19.36zv  4453  ralsnsg  4615  eldifvsn  4741  ssunsn2  4771  iunconst  4944  iinconst  4945  iuneqconst  4946  relsng  5752  dmxp  5880  opelres  5946  ordsseleq  6348  ordequn  6424  funssres  6538  fncnv  6567  ffrnbd  6679  fresaun  6707  dff1o5  6785  tz6.12c  6858  funimass4  6900  fndmdifeq0  6992  fneqeql2  6995  unpreima  7011  dffo3  7050  dffo3f  7054  fnnfpeq0  7128  funfvima  7180  f1eqcocnv  7251  fliftf  7265  isocnv3  7282  isomin  7287  eloprabga  7471  mpo2eqb  7494  elpwun  7718  dfom2  7814  opabex3d  7913  opabex3rd  7914  opabex3  7915  f1oweALT  7920  fnwelem  8076  mptsuppd  8132  dfrecs3  8307  oe0m1  8451  oarec  8492  eldifsucnn  8595  naddsuc2  8632  boxcutc  8884  ordunifi  9195  ttrclselem2  9642  r1fin  9692  rankr1c  9740  iscard  9894  iscard2  9895  cardval2  9910  dfac3  10038  kmlem8  10075  xrlenlt  11205  ltxrlt  11211  negcon2  11442  mulne0b  11786  dfinfre  12132  crne0  12147  elznn  12535  zmax  12890  elfznelfzo  13723  modmuladdnn0  13872  hashneq0  14321  xpcogend  14931  sqrtneglem  15223  rexfiuz  15305  rexanuz2  15307  sumsplit  15725  fsum2dlem  15727  odd2np1  16305  divalgb  16368  gcdcllem2  16464  mrcidb2  17579  fncnvimaeqv  18081  qusecsub  19805  domnmuln0  20681  acsfn1p  20771  lbsacsbs  21150  islpir2  21324  islinds2  21807  islbs4  21826  mplcoe1  22029  mplcoe5  22032  mamucl  22380  mavmulcl  22526  mdetunilem8  22598  iscld4  23044  isconn2  23393  kgencn  23535  tx1cn  23588  tx2cn  23589  elmptrab  23806  isfbas  23808  fbfinnfr  23820  cnfcf  24021  fmucndlem  24269  prdsxmslem2  24508  blval2  24541  cnbl0  24752  cnblcld  24753  metcld  25287  ismbf  25609  ismbfcn  25610  itg1val2  25665  itg2split  25730  itg2monolem1  25731  aannenlem1  26309  pilem1  26433  sinq34lt0t  26490  ellogrn  26540  logeftb  26564  gausslemma2dlem1a  27346  sltssnb  27779  bdayle  27926  elznns  28412  zsoring  28419  readdscl  28509  ercgrg  28603  elntg2  29072  usgredgffibi  29411  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  32737  1stpreima  32799  2ndpreima  32800  creq0  32828  hashgt1  32900  isunit3  33321  isdrng4  33375  qusxpid  33442  lindflbs  33458  dvdsruassoi  33463  dvdsruasso  33464  dvdsrspss  33466  unitprodclb  33468  lsmsnorb  33470  nsgqusf1olem3  33494  qsfld  33577  esplyind  33738  qtophaus  34000  prsdm  34078  prsrn  34079  1stmbfm  34424  2ndmbfm  34425  eulerpartlemn  34545  reprdifc  34791  circlemeth  34804  bnj1454  35004  bnj984  35114  vonf1owev  35310  dffun10  36114  hfext  36385  isfne4b  36543  neifg  36573  taupilem3  37653  topdifinfindis  37680  topdifinffinlem  37681  finxpsuclem  37731  nlpineqsn  37742  wl-ifp-ncond1  37798  poimirlem23  37982  poimirlem26  37985  cnambfre  38007  0totbnd  38112  opelvvdif  38603  inecmo  38694  brxrn  38722  brin2  38777  suceqsneq  38823  eleccossin  38912  dffunsALTV2  39108  dffunsALTV3  39109  dffunsALTV4  39110  elfunsALTV2  39117  elfunsALTV3  39118  elfunsALTV4  39119  elfunsALTV5  39120  dfdisjs2  39133  eldisjs2  39159  disjres  39183  cvrval2  39738  cvrnbtwn2  39739  cvrnbtwn4  39743  hlateq  39863  islpln5  39999  islvol5  40043  pmap11  40226  4atex  40540  cdleme0ex2N  40688  cdlemefrs29pre00  40859  diaord  41511  dihmeetlem13N  41783  lcfl1  41956  lcfls1N  41999  mapdpglem3  42139  isnacs2  43156  mrefg3  43158  pw2f1ocnv  43487  unielss  43668  onmaxnelsup  43673  onsupnmax  43678  onov0suclim  43724  cantnf2  43775  ordsssucb  43785  relexp0eq  44150  frege124d  44210  uneqsn  44474  k0004lem1  44596  sbcoreleleq  44984  modelac8prim  45441  r19.28zf  45611  climreeq  46065  funressnfv  47507  2timesltsqm1  47843  fmtnorec2lem  48021  sclnbgrelself  48340  gpgiedgdmel  48541  gpgedgel  48542  eenglngeehlnmlem1  49229  eenglngeehlnmlem2  49230  rrx2linest2  49236  itsclinecirc0b  49266  map0cor  49346  ipolublem  49477  ipoglblem  49480  functermc  49999