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  534  cad1  1610  necon2abid  2973  reueubd  3383  reu8  3726  sbc6gOLD  3805  r19.28z  4498  r19.37zv  4502  r19.45zv  4503  r19.44zv  4504  r19.27z  4505  r19.36zv  4507  ralidmOLD  4516  ralsnsg  4673  eldifvsn  4801  ssunsn2  4831  iunconst  5005  iinconst  5006  iuneqconst  5007  relsng  5802  opelres  5990  ordsseleq  6398  ordequn  6472  funssres  6596  fncnv  6625  ffrnbd  6736  fresaun  6766  dff1o5  6845  tz6.12c  6916  funimass4  6960  fndmdifeq0  7050  fneqeql2  7053  unpreima  7069  dffo3  7109  dffo3f  7113  fnnfpeq0  7185  funfvima  7240  f1eqcocnv  7308  fliftf  7320  isocnv3  7337  isomin  7342  eloprabga  7526  eloprabgaOLD  7527  mpo2eqb  7551  elpwun  7770  dfom2  7871  opabex3d  7968  opabex3rd  7969  opabex3  7970  f1oweALT  7975  fnwelem  8134  mptsuppd  8190  dfrecs3  8391  dfrecs3OLD  8392  oe0m1  8540  oarec  8581  eldifsucnn  8683  boxcutc  8958  ordunifi  9316  ttrclselem2  9749  r1fin  9796  rankr1c  9844  iscard  9998  iscard2  9999  cardval2  10014  dfac3  10144  kmlem8  10180  infinf  10589  xrlenlt  11309  ltxrlt  11314  negcon2  11543  mulne0b  11885  dfinfre  12225  crne0  12235  elznn  12604  zmax  12959  elfznelfzo  13769  modmuladdnn0  13912  hashneq0  14355  xpcogend  14953  sqrtneglem  15245  rexfiuz  15326  rexanuz2  15328  sumsplit  15746  fsum2dlem  15748  odd2np1  16317  divalgb  16380  gcdcllem2  16474  mrcidb2  17597  fncnvimaeqv  18109  qusecsub  19794  acsfn1p  20691  lbsacsbs  21048  islpir2  21224  domnmuln0  21249  islinds2  21751  islbs4  21770  mplcoe1  21982  mplcoe5  21985  mamucl  22331  mavmulcl  22479  mdetunilem8  22551  iscld4  22999  isconn2  23348  kgencn  23490  tx1cn  23543  tx2cn  23544  elmptrab  23761  isfbas  23763  fbfinnfr  23775  cnfcf  23976  fmucndlem  24226  prdsxmslem2  24468  blval2  24501  cnbl0  24720  cnblcld  24721  metcld  25264  ismbf  25587  ismbfcn  25588  itg1val2  25643  itg2split  25709  itg2monolem1  25710  aannenlem1  26293  pilem1  26418  sinq34lt0t  26474  ellogrn  26523  logeftb  26547  gausslemma2dlem1a  27328  readdscl  28283  ercgrg  28377  elntg2  28852  usgredgffibi  29193  vtxd0nedgb  29358  vdiscusgrb  29400  upgrspthswlk  29608  s3wwlks2on  29823  clwwlknonwwlknonb  29972  frgrncvvdeqlem2  30166  ch0pss  31311  h1de2ctlem  31421  adjsym  31699  eigposi  31702  dfadj2  31751  elnlfn  31794  xppreima  32489  1stpreima  32543  2ndpreima  32544  creq0  32574  hashgt1  32634  isdrng4  33044  qusxpid  33135  dvdsruassoi  33149  dvdsruasso  33150  dvdsrspss  33152  lindflbs  33156  lsmsnorb  33162  nsgqusf1olem3  33187  qsfld  33271  qtophaus  33507  prsdm  33585  prsrn  33586  1stmbfm  33950  2ndmbfm  33951  eulerpartlemn  34071  reprdifc  34329  circlemeth  34342  bnj1454  34543  bnj984  34653  dffun10  35580  hfext  35849  isfne4b  35895  neifg  35925  taupilem3  36868  topdifinfindis  36895  topdifinffinlem  36896  finxpsuclem  36946  nlpineqsn  36957  wl-ifp-ncond1  37013  poimirlem23  37186  poimirlem26  37189  cnambfre  37211  0totbnd  37316  suceqsneq  37777  opelvvdif  37800  inecmo  37896  brxrn  37915  brin2  37950  eleccossin  38024  dffunsALTV2  38225  dffunsALTV3  38226  dffunsALTV4  38227  elfunsALTV2  38234  elfunsALTV3  38235  elfunsALTV4  38236  elfunsALTV5  38237  dfdisjs2  38250  eldisjs2  38264  disjres  38285  cvrval2  38815  cvrnbtwn2  38816  cvrnbtwn4  38820  hlateq  38941  islpln5  39077  islvol5  39121  pmap11  39304  4atex  39618  cdleme0ex2N  39766  cdlemefrs29pre00  39937  diaord  40589  dihmeetlem13N  40861  lcfl1  41034  lcfls1N  41077  mapdpglem3  41217  isnacs2  42191  mrefg3  42193  pw2f1ocnv  42523  unielss  42711  onmaxnelsup  42716  onsupnmax  42721  onov0suclim  42768  cantnf2  42819  ordsssucb  42829  naddsuc2  42887  relexp0eq  43196  frege124d  43256  uneqsn  43520  k0004lem1  43642  sbcoreleleq  44039  r19.28zf  44594  climreeq  45064  funressnfv  46488  fmtnorec2lem  46945  sclnbgrelself  47246  eenglngeehlnmlem1  47922  eenglngeehlnmlem2  47923  rrx2linest2  47929  itsclinecirc0b  47959  map0cor  48019  ipolublem  48109  ipoglblem  48112