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 223	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 288	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  1619  necon2abid  2987  reueubd  3368  reu8  3669  sbc6gOLD  3748  r19.28z  4429  r19.37zv  4433  r19.45zv  4434  r19.44zv  4435  r19.27z  4436  r19.36zv  4438  ralidmOLD  4447  ralsnsg  4605  eldifvsn  4731  ssunsn2  4761  iunconst  4934  iinconst  4935  iuneqconst  4936  relsng  5713  opelres  5900  ordsseleq  6299  ordequn  6370  funssres  6485  fncnv  6514  ffrnbd  6625  fresaun  6654  dff1o5  6734  funimass4  6843  fndmdifeq0  6930  fneqeql2  6933  unpreima  6949  dffo3  6987  fnnfpeq0  7059  funfvima  7115  f1eqcocnv  7182  f1eqcocnvOLD  7183  fliftf  7195  isocnv3  7212  isomin  7217  eloprabga  7391  eloprabgaOLD  7392  mpo2eqb  7415  elpwun  7628  dfom2  7723  opabex3d  7817  opabex3rd  7818  opabex3  7819  f1oweALT  7824  fnwelem  7981  mptsuppd  8012  dfrecs3  8212  dfrecs3OLD  8213  oe0m1  8360  oarec  8402  eldifsucnn  8503  boxcutc  8738  ordunifi  9073  ttrclselem2  9493  r1fin  9540  rankr1c  9588  iscard  9742  iscard2  9743  cardval2  9758  dfac3  9886  kmlem8  9922  infinf  10331  xrlenlt  11049  ltxrlt  11054  negcon2  11283  mulne0b  11625  dfinfre  11965  crne0  11975  elznn  12344  zmax  12694  elfznelfzo  13501  modmuladdnn0  13644  hashneq0  14088  xpcogend  14694  sqrtneglem  14987  rexfiuz  15068  rexanuz2  15070  sumsplit  15489  fsum2dlem  15491  odd2np1  16059  divalgb  16122  gcdcllem2  16216  mrcidb2  17336  fncnvimaeqv  17845  acsfn1p  20076  lbsacsbs  20427  islpir2  20531  domnmuln0  20578  islinds2  21029  islbs4  21048  mplcoe1  21247  mplcoe5  21250  mamucl  21557  mavmulcl  21705  mdetunilem8  21777  iscld4  22225  isconn2  22574  kgencn  22716  tx1cn  22769  tx2cn  22770  elmptrab  22987  isfbas  22989  fbfinnfr  23001  cnfcf  23202  fmucndlem  23452  prdsxmslem2  23694  blval2  23727  cnbl0  23946  cnblcld  23947  metcld  24479  ismbf  24801  ismbfcn  24802  itg1val2  24857  itg2split  24923  itg2monolem1  24924  aannenlem1  25497  pilem1  25619  sinq34lt0t  25675  ellogrn  25724  logeftb  25748  gausslemma2dlem1a  26522  ercgrg  26887  elntg2  27362  usgredgffibi  27700  vtxd0nedgb  27864  vdiscusgrb  27906  upgrspthswlk  28115  s3wwlks2on  28330  clwwlknonwwlknonb  28479  frgrncvvdeqlem2  28673  ch0pss  29816  h1de2ctlem  29926  adjsym  30204  eigposi  30207  dfadj2  30256  elnlfn  30299  xppreima  30992  1stpreima  31048  2ndpreima  31049  creq0  31079  hashgt1  31137  qusxpid  31568  lindflbs  31583  lsmsnorb  31588  nsgqusf1olem3  31609  qtophaus  31795  prsdm  31873  prsrn  31874  1stmbfm  32236  2ndmbfm  32237  eulerpartlemn  32357  reprdifc  32616  circlemeth  32629  bnj1454  32831  bnj984  32941  xpord3pred  33807  dffun10  34225  hfext  34494  isfne4b  34539  neifg  34569  taupilem3  35499  topdifinfindis  35526  topdifinffinlem  35527  finxpsuclem  35577  nlpineqsn  35588  wl-ifp-ncond1  35644  poimirlem23  35809  poimirlem26  35812  cnambfre  35834  0totbnd  35940  opelvvdif  36406  inecmo  36494  brxrn  36511  brin2  36542  eleccossin  36608  dffunsALTV2  36802  dffunsALTV3  36803  dffunsALTV4  36804  elfunsALTV2  36811  elfunsALTV3  36812  elfunsALTV4  36813  elfunsALTV5  36814  dfdisjs2  36827  eldisjs2  36841  cvrval2  37295  cvrnbtwn2  37296  cvrnbtwn4  37300  hlateq  37420  islpln5  37556  islvol5  37600  pmap11  37783  4atex  38097  cdleme0ex2N  38245  cdlemefrs29pre00  38416  diaord  39068  dihmeetlem13N  39340  lcfl1  39513  lcfls1N  39556  mapdpglem3  39696  isnacs2  40535  mrefg3  40537  pw2f1ocnv  40866  nlimsuc  41055  relexp0eq  41316  frege124d  41376  uneqsn  41640  k0004lem1  41764  sbcoreleleq  42162  dffo3f  42724  climreeq  43161  funressnfv  44548  fmtnorec2lem  45005  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2linest2  46101  itsclinecirc0b  46131  map0cor  46193  ipolublem  46283  ipoglblem  46286