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  2974  reueubd  3359  issetft  3445  reu8  3679  r19.28z  4442  r19.37zv  4447  r19.45zv  4448  r19.44zv  4449  r19.27z  4450  r19.36zv  4452  ralsnsg  4614  eldifvsn  4742  ssunsn2  4770  iunconst  4943  iinconst  4944  iuneqconst  4945  relsng  5757  dmxp  5884  opelres  5950  ordsseleq  6352  ordequn  6428  funssres  6542  fncnv  6571  ffrnbd  6683  fresaun  6711  dff1o5  6789  tz6.12c  6862  funimass4  6904  fndmdifeq0  6996  fneqeql2  6999  unpreima  7015  dffo3  7054  dffo3f  7058  fnnfpeq0  7133  funfvima  7185  f1eqcocnv  7256  fliftf  7270  isocnv3  7287  isomin  7292  eloprabga  7476  mpo2eqb  7499  elpwun  7723  dfom2  7819  opabex3d  7918  opabex3rd  7919  opabex3  7920  f1oweALT  7925  fnwelem  8081  mptsuppd  8137  dfrecs3  8312  oe0m1  8456  oarec  8497  eldifsucnn  8600  naddsuc2  8637  boxcutc  8889  ordunifi  9200  ttrclselem2  9647  r1fin  9697  rankr1c  9745  iscard  9899  iscard2  9900  cardval2  9915  dfac3  10043  kmlem8  10080  xrlenlt  11210  ltxrlt  11216  negcon2  11447  mulne0b  11791  dfinfre  12137  crne0  12152  elznn  12540  zmax  12895  elfznelfzo  13728  modmuladdnn0  13877  hashneq0  14326  xpcogend  14936  sqrtneglem  15228  rexfiuz  15310  rexanuz2  15312  sumsplit  15730  fsum2dlem  15732  odd2np1  16310  divalgb  16373  gcdcllem2  16469  mrcidb2  17584  fncnvimaeqv  18086  qusecsub  19810  domnmuln0  20686  acsfn1p  20776  lbsacsbs  21154  islpir2  21328  islinds2  21793  islbs4  21812  mplcoe1  22015  mplcoe5  22018  mamucl  22366  mavmulcl  22512  mdetunilem8  22584  iscld4  23030  isconn2  23379  kgencn  23521  tx1cn  23574  tx2cn  23575  elmptrab  23792  isfbas  23794  fbfinnfr  23806  cnfcf  24007  fmucndlem  24255  prdsxmslem2  24494  blval2  24527  cnbl0  24738  cnblcld  24739  metcld  25273  ismbf  25595  ismbfcn  25596  itg1val2  25651  itg2split  25716  itg2monolem1  25717  aannenlem1  26294  pilem1  26416  sinq34lt0t  26473  ellogrn  26523  logeftb  26547  gausslemma2dlem1a  27328  sltssnb  27761  bdayle  27908  elznns  28394  zsoring  28401  readdscl  28491  ercgrg  28585  elntg2  29054  usgredgffibi  29393  vtxd0nedgb  29557  vdiscusgrb  29599  upgrspthswlk  29806  s3wwlks2on  30024  sps3wwlks2on  30025  clwwlknonwwlknonb  30176  frgrncvvdeqlem2  30370  ch0pss  31516  h1de2ctlem  31626  adjsym  31904  eigposi  31907  dfadj2  31956  elnlfn  31999  xppreima  32718  1stpreima  32780  2ndpreima  32781  creq0  32809  hashgt1  32881  isunit3  33302  isdrng4  33356  qusxpid  33423  lindflbs  33439  dvdsruassoi  33444  dvdsruasso  33445  dvdsrspss  33447  unitprodclb  33449  lsmsnorb  33451  nsgqusf1olem3  33475  qsfld  33558  esplyind  33719  qtophaus  33980  prsdm  34058  prsrn  34059  1stmbfm  34404  2ndmbfm  34405  eulerpartlemn  34525  reprdifc  34771  circlemeth  34784  bnj1454  34984  bnj984  35094  vonf1owev  35290  dffun10  36094  hfext  36365  isfne4b  36523  neifg  36553  taupilem3  37633  topdifinfindis  37662  topdifinffinlem  37663  finxpsuclem  37713  nlpineqsn  37724  wl-ifp-ncond1  37780  poimirlem23  37964  poimirlem26  37967  cnambfre  37989  0totbnd  38094  opelvvdif  38585  inecmo  38676  brxrn  38704  brin2  38759  suceqsneq  38805  eleccossin  38894  dffunsALTV2  39090  dffunsALTV3  39091  dffunsALTV4  39092  elfunsALTV2  39099  elfunsALTV3  39100  elfunsALTV4  39101  elfunsALTV5  39102  dfdisjs2  39115  eldisjs2  39141  disjres  39165  cvrval2  39720  cvrnbtwn2  39721  cvrnbtwn4  39725  hlateq  39845  islpln5  39981  islvol5  40025  pmap11  40208  4atex  40522  cdleme0ex2N  40670  cdlemefrs29pre00  40841  diaord  41493  dihmeetlem13N  41765  lcfl1  41938  lcfls1N  41981  mapdpglem3  42121  isnacs2  43138  mrefg3  43140  pw2f1ocnv  43465  unielss  43646  onmaxnelsup  43651  onsupnmax  43656  onov0suclim  43702  cantnf2  43753  ordsssucb  43763  relexp0eq  44128  frege124d  44188  uneqsn  44452  k0004lem1  44574  sbcoreleleq  44962  modelac8prim  45419  r19.28zf  45589  climreeq  46043  funressnfv  47491  2timesltsqm1  47827  fmtnorec2lem  48005  sclnbgrelself  48324  gpgiedgdmel  48525  gpgedgel  48526  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2linest2  49220  itsclinecirc0b  49250  map0cor  49330  ipolublem  49461  ipoglblem  49464  functermc  49983