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  3727  sbc6gOLD  3806  r19.28z  4493  r19.37zv  4497  r19.45zv  4498  r19.44zv  4499  r19.27z  4500  r19.36zv  4502  ralidmOLD  4511  ralsnsg  4668  eldifvsn  4796  ssunsn2  4826  iunconst  5002  iinconst  5003  iuneqconst  5004  relsng  5796  opelres  5982  ordsseleq  6385  ordequn  6459  funssres  6584  fncnv  6613  ffrnbd  6723  fresaun  6752  dff1o5  6832  tz6.12c  6903  funimass4  6946  fndmdifeq0  7033  fneqeql2  7036  unpreima  7052  dffo3  7091  fnnfpeq0  7163  funfvima  7219  f1eqcocnv  7286  f1eqcocnvOLD  7287  fliftf  7299  isocnv3  7316  isomin  7321  eloprabga  7503  eloprabgaOLD  7504  mpo2eqb  7528  elpwun  7743  dfom2  7844  opabex3d  7939  opabex3rd  7940  opabex3  7941  f1oweALT  7946  fnwelem  8104  mptsuppd  8159  dfrecs3  8359  dfrecs3OLD  8360  oe0m1  8508  oarec  8550  eldifsucnn  8651  boxcutc  8923  ordunifi  9281  ttrclselem2  9708  r1fin  9755  rankr1c  9803  iscard  9957  iscard2  9958  cardval2  9973  dfac3  10103  kmlem8  10139  infinf  10548  xrlenlt  11266  ltxrlt  11271  negcon2  11500  mulne0b  11842  dfinfre  12182  crne0  12192  elznn  12561  zmax  12916  elfznelfzo  13724  modmuladdnn0  13867  hashneq0  14311  xpcogend  14908  sqrtneglem  15200  rexfiuz  15281  rexanuz2  15283  sumsplit  15701  fsum2dlem  15703  odd2np1  16271  divalgb  16334  gcdcllem2  16428  mrcidb2  17549  fncnvimaeqv  18058  qusecsub  19686  acsfn1p  20392  lbsacsbs  20746  islpir2  20865  domnmuln0  20890  islinds2  21341  islbs4  21360  mplcoe1  21560  mplcoe5  21563  mamucl  21870  mavmulcl  22018  mdetunilem8  22090  iscld4  22538  isconn2  22887  kgencn  23029  tx1cn  23082  tx2cn  23083  elmptrab  23300  isfbas  23302  fbfinnfr  23314  cnfcf  23515  fmucndlem  23765  prdsxmslem2  24007  blval2  24040  cnbl0  24259  cnblcld  24260  metcld  24792  ismbf  25114  ismbfcn  25115  itg1val2  25170  itg2split  25236  itg2monolem1  25237  aannenlem1  25810  pilem1  25932  sinq34lt0t  25988  ellogrn  26037  logeftb  26061  gausslemma2dlem1a  26835  ercgrg  27735  elntg2  28210  usgredgffibi  28548  vtxd0nedgb  28712  vdiscusgrb  28754  upgrspthswlk  28962  s3wwlks2on  29177  clwwlknonwwlknonb  29326  frgrncvvdeqlem2  29520  ch0pss  30663  h1de2ctlem  30773  adjsym  31051  eigposi  31054  dfadj2  31103  elnlfn  31146  xppreima  31840  1stpreima  31899  2ndpreima  31900  creq0  31931  hashgt1  31991  isdrng4  32357  qusxpid  32437  lindflbs  32453  lsmsnorb  32459  nsgqusf1olem3  32482  qsfld  32558  qtophaus  32747  prsdm  32825  prsrn  32826  1stmbfm  33190  2ndmbfm  33191  eulerpartlemn  33311  reprdifc  33570  circlemeth  33583  bnj1454  33784  bnj984  33894  dffun10  34817  hfext  35086  isfne4b  35131  neifg  35161  taupilem3  36105  topdifinfindis  36132  topdifinffinlem  36133  finxpsuclem  36183  nlpineqsn  36194  wl-ifp-ncond1  36250  poimirlem23  36416  poimirlem26  36419  cnambfre  36441  0totbnd  36547  suceqsneq  37009  opelvvdif  37033  inecmo  37130  brxrn  37150  brin2  37185  eleccossin  37259  dffunsALTV2  37460  dffunsALTV3  37461  dffunsALTV4  37462  elfunsALTV2  37469  elfunsALTV3  37470  elfunsALTV4  37471  elfunsALTV5  37472  dfdisjs2  37485  eldisjs2  37499  disjres  37520  cvrval2  38050  cvrnbtwn2  38051  cvrnbtwn4  38055  hlateq  38176  islpln5  38312  islvol5  38356  pmap11  38539  4atex  38853  cdleme0ex2N  39001  cdlemefrs29pre00  39172  diaord  39824  dihmeetlem13N  40096  lcfl1  40269  lcfls1N  40312  mapdpglem3  40452  isnacs2  41315  mrefg3  41317  pw2f1ocnv  41647  unielss  41838  onmaxnelsup  41843  onsupnmax  41848  onov0suclim  41895  cantnf2  41946  ordsssucb  41956  naddsuc2  42014  relexp0eq  42323  frege124d  42383  uneqsn  42647  k0004lem1  42769  sbcoreleleq  43167  r19.28zf  43724  dffo3f  43748  climreeq  44202  funressnfv  45626  fmtnorec2lem  46083  eenglngeehlnmlem1  47263  eenglngeehlnmlem2  47264  rrx2linest2  47270  itsclinecirc0b  47300  map0cor  47361  ipolublem  47451  ipoglblem  47454