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  5748  dmxp  5876  opelres  5942  ordsseleq  6344  ordequn  6420  funssres  6534  fncnv  6563  ffrnbd  6675  fresaun  6703  dff1o5  6781  tz6.12c  6854  funimass4  6896  fndmdifeq0  6988  fneqeql2  6991  unpreima  7007  dffo3  7046  dffo3f  7050  fnnfpeq0  7124  funfvima  7176  f1eqcocnv  7247  fliftf  7261  isocnv3  7278  isomin  7283  eloprabga  7467  mpo2eqb  7490  elpwun  7714  dfom2  7810  opabex3d  7909  opabex3rd  7910  opabex3  7911  f1oweALT  7916  fnwelem  8072  mptsuppd  8128  dfrecs3  8303  oe0m1  8447  oarec  8488  eldifsucnn  8591  naddsuc2  8628  boxcutc  8880  ordunifi  9191  ttrclselem2  9636  r1fin  9686  rankr1c  9734  iscard  9888  iscard2  9889  cardval2  9904  dfac3  10032  kmlem8  10069  xrlenlt  11199  ltxrlt  11205  negcon2  11436  mulne0b  11780  dfinfre  12126  crne0  12141  elznn  12529  zmax  12884  elfznelfzo  13717  modmuladdnn0  13866  hashneq0  14315  xpcogend  14925  sqrtneglem  15217  rexfiuz  15299  rexanuz2  15301  sumsplit  15719  fsum2dlem  15721  odd2np1  16299  divalgb  16362  gcdcllem2  16458  mrcidb2  17573  fncnvimaeqv  18075  qusecsub  19799  domnmuln0  20675  acsfn1p  20765  lbsacsbs  21144  islpir2  21318  islinds2  21801  islbs4  21820  mplcoe1  22024  mplcoe5  22027  mamucl  22375  mavmulcl  22521  mdetunilem8  22593  iscld4  23039  isconn2  23388  kgencn  23530  tx1cn  23583  tx2cn  23584  elmptrab  23801  isfbas  23803  fbfinnfr  23815  cnfcf  24016  fmucndlem  24264  prdsxmslem2  24503  blval2  24536  cnbl0  24747  cnblcld  24748  metcld  25282  ismbf  25604  ismbfcn  25605  itg1val2  25660  itg2split  25725  itg2monolem1  25726  aannenlem1  26307  pilem1  26432  sinq34lt0t  26489  ellogrn  26539  logeftb  26563  gausslemma2dlem1a  27347  sltssnb  27780  bdayle  27927  elznns  28413  zsoring  28420  readdscl  28510  ercgrg  28604  elntg2  29073  usgredgffibi  29412  vtxd0nedgb  29577  vdiscusgrb  29619  upgrspthswlk  29826  s3wwlks2on  30044  sps3wwlks2on  30045  clwwlknonwwlknonb  30196  frgrncvvdeqlem2  30390  ch0pss  31536  h1de2ctlem  31646  adjsym  31924  eigposi  31927  dfadj2  31976  elnlfn  32019  xppreima  32738  1stpreima  32800  2ndpreima  32801  creq0  32829  hashgt1  32901  isunit3  33322  isdrng4  33376  qusxpid  33443  lindflbs  33459  dvdsruassoi  33464  dvdsruasso  33465  dvdsrspss  33467  unitprodclb  33469  lsmsnorb  33471  nsgqusf1olem3  33495  qsfld  33578  esplyind  33739  qtophaus  34001  prsdm  34079  prsrn  34080  1stmbfm  34425  2ndmbfm  34426  eulerpartlemn  34546  reprdifc  34792  circlemeth  34805  bnj1454  35005  bnj984  35115  vonf1owev  35311  dffun10  36115  hfext  36386  isfne4b  36544  neifg  36574  taupilem3  37646  topdifinfindis  37673  topdifinffinlem  37674  finxpsuclem  37724  nlpineqsn  37735  wl-ifp-ncond1  37791  poimirlem23  37975  poimirlem26  37978  cnambfre  38000  0totbnd  38105  opelvvdif  38596  inecmo  38687  brxrn  38715  brin2  38770  suceqsneq  38816  eleccossin  38905  dffunsALTV2  39101  dffunsALTV3  39102  dffunsALTV4  39103  elfunsALTV2  39110  elfunsALTV3  39111  elfunsALTV4  39112  elfunsALTV5  39113  dfdisjs2  39126  eldisjs2  39152  disjres  39176  cvrval2  39731  cvrnbtwn2  39732  cvrnbtwn4  39736  hlateq  39856  islpln5  39992  islvol5  40036  pmap11  40219  4atex  40533  cdleme0ex2N  40681  cdlemefrs29pre00  40852  diaord  41504  dihmeetlem13N  41776  lcfl1  41949  lcfls1N  41992  mapdpglem3  42132  isnacs2  43149  mrefg3  43151  pw2f1ocnv  43480  unielss  43661  onmaxnelsup  43666  onsupnmax  43671  onov0suclim  43717  cantnf2  43768  ordsssucb  43778  relexp0eq  44143  frege124d  44203  uneqsn  44467  k0004lem1  44589  sbcoreleleq  44977  modelac8prim  45434  r19.28zf  45604  climreeq  46058  funressnfv  47488  2timesltsqm1  47824  fmtnorec2lem  48002  sclnbgrelself  48321  gpgiedgdmel  48522  gpgedgel  48523  eenglngeehlnmlem1  49210  eenglngeehlnmlem2  49211  rrx2linest2  49217  itsclinecirc0b  49247  map0cor  49327  ipolublem  49458  ipoglblem  49461  functermc  49980