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  537  cad1  1619  necon2abid  2984  reueubd  3396  reu8  3730  sbc6gOLD  3809  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  5007  iinconst  5008  iuneqconst  5009  relsng  5802  opelres  5988  ordsseleq  6394  ordequn  6468  funssres  6593  fncnv  6622  ffrnbd  6734  fresaun  6763  dff1o5  6843  tz6.12c  6914  funimass4  6957  fndmdifeq0  7046  fneqeql2  7049  unpreima  7065  dffo3  7104  fnnfpeq0  7176  funfvima  7232  f1eqcocnv  7299  f1eqcocnvOLD  7300  fliftf  7312  isocnv3  7329  isomin  7334  eloprabga  7516  eloprabgaOLD  7517  mpo2eqb  7541  elpwun  7756  dfom2  7857  opabex3d  7952  opabex3rd  7953  opabex3  7954  f1oweALT  7959  fnwelem  8117  mptsuppd  8172  dfrecs3  8372  dfrecs3OLD  8373  oe0m1  8521  oarec  8562  eldifsucnn  8663  boxcutc  8935  ordunifi  9293  ttrclselem2  9721  r1fin  9768  rankr1c  9816  iscard  9970  iscard2  9971  cardval2  9986  dfac3  10116  kmlem8  10152  infinf  10561  xrlenlt  11279  ltxrlt  11284  negcon2  11513  mulne0b  11855  dfinfre  12195  crne0  12205  elznn  12574  zmax  12929  elfznelfzo  13737  modmuladdnn0  13880  hashneq0  14324  xpcogend  14921  sqrtneglem  15213  rexfiuz  15294  rexanuz2  15296  sumsplit  15714  fsum2dlem  15716  odd2np1  16284  divalgb  16347  gcdcllem2  16441  mrcidb2  17562  fncnvimaeqv  18071  qusecsub  19703  acsfn1p  20415  lbsacsbs  20769  islpir2  20889  domnmuln0  20914  islinds2  21368  islbs4  21387  mplcoe1  21592  mplcoe5  21595  mamucl  21901  mavmulcl  22049  mdetunilem8  22121  iscld4  22569  isconn2  22918  kgencn  23060  tx1cn  23113  tx2cn  23114  elmptrab  23331  isfbas  23333  fbfinnfr  23345  cnfcf  23546  fmucndlem  23796  prdsxmslem2  24038  blval2  24071  cnbl0  24290  cnblcld  24291  metcld  24823  ismbf  25145  ismbfcn  25146  itg1val2  25201  itg2split  25267  itg2monolem1  25268  aannenlem1  25841  pilem1  25963  sinq34lt0t  26019  ellogrn  26068  logeftb  26092  gausslemma2dlem1a  26868  ercgrg  27799  elntg2  28274  usgredgffibi  28612  vtxd0nedgb  28776  vdiscusgrb  28818  upgrspthswlk  29026  s3wwlks2on  29241  clwwlknonwwlknonb  29390  frgrncvvdeqlem2  29584  ch0pss  30729  h1de2ctlem  30839  adjsym  31117  eigposi  31120  dfadj2  31169  elnlfn  31212  xppreima  31902  1stpreima  31959  2ndpreima  31960  creq0  31991  hashgt1  32051  isdrng4  32426  qusxpid  32506  dvdsruassoi  32520  dvdsruasso  32521  dvdsrspss  32522  lindflbs  32526  lsmsnorb  32532  nsgqusf1olem3  32557  qsfld  32643  qtophaus  32847  prsdm  32925  prsrn  32926  1stmbfm  33290  2ndmbfm  33291  eulerpartlemn  33411  reprdifc  33670  circlemeth  33683  bnj1454  33884  bnj984  33994  dffun10  34917  hfext  35186  isfne4b  35274  neifg  35304  taupilem3  36248  topdifinfindis  36275  topdifinffinlem  36276  finxpsuclem  36326  nlpineqsn  36337  wl-ifp-ncond1  36393  poimirlem23  36559  poimirlem26  36562  cnambfre  36584  0totbnd  36689  suceqsneq  37151  opelvvdif  37175  inecmo  37272  brxrn  37292  brin2  37327  eleccossin  37401  dffunsALTV2  37602  dffunsALTV3  37603  dffunsALTV4  37604  elfunsALTV2  37611  elfunsALTV3  37612  elfunsALTV4  37613  elfunsALTV5  37614  dfdisjs2  37627  eldisjs2  37641  disjres  37662  cvrval2  38192  cvrnbtwn2  38193  cvrnbtwn4  38197  hlateq  38318  islpln5  38454  islvol5  38498  pmap11  38681  4atex  38995  cdleme0ex2N  39143  cdlemefrs29pre00  39314  diaord  39966  dihmeetlem13N  40238  lcfl1  40411  lcfls1N  40454  mapdpglem3  40594  isnacs2  41492  mrefg3  41494  pw2f1ocnv  41824  unielss  42015  onmaxnelsup  42020  onsupnmax  42025  onov0suclim  42072  cantnf2  42123  ordsssucb  42133  naddsuc2  42191  relexp0eq  42500  frege124d  42560  uneqsn  42824  k0004lem1  42946  sbcoreleleq  43344  r19.28zf  43901  dffo3f  43925  climreeq  44377  funressnfv  45801  fmtnorec2lem  46258  eenglngeehlnmlem1  47471  eenglngeehlnmlem2  47472  rrx2linest2  47478  itsclinecirc0b  47508  map0cor  47569  ipolublem  47659  ipoglblem  47662