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  1616  necon2abid  2982  reueubd  3398  issetft  3495  reu8  3738  r19.28z  4497  r19.37zv  4501  r19.45zv  4502  r19.44zv  4503  r19.27z  4504  r19.36zv  4506  ralsnsg  4669  eldifvsn  4796  ssunsn2  4826  iunconst  5000  iinconst  5001  iuneqconst  5002  relsng  5810  dmxp  5938  opelres  6002  ordsseleq  6412  ordequn  6486  funssres  6609  fncnv  6638  ffrnbd  6750  fresaun  6778  dff1o5  6856  tz6.12c  6927  funimass4  6972  fndmdifeq0  7063  fneqeql2  7066  unpreima  7082  dffo3  7121  dffo3f  7125  fnnfpeq0  7199  funfvima  7251  f1eqcocnv  7322  fliftf  7336  isocnv3  7353  isomin  7358  eloprabga  7543  mpo2eqb  7566  elpwun  7790  dfom2  7890  opabex3d  7991  opabex3rd  7992  opabex3  7993  f1oweALT  7998  fnwelem  8157  mptsuppd  8213  dfrecs3  8413  dfrecs3OLD  8414  oe0m1  8560  oarec  8601  eldifsucnn  8703  naddsuc2  8740  boxcutc  8982  ordunifi  9327  ttrclselem2  9767  r1fin  9814  rankr1c  9862  iscard  10016  iscard2  10017  cardval2  10032  dfac3  10162  kmlem8  10199  infinf  10607  xrlenlt  11327  ltxrlt  11332  negcon2  11563  mulne0b  11905  dfinfre  12250  crne0  12260  elznn  12631  zmax  12988  elfznelfzo  13812  modmuladdnn0  13957  hashneq0  14404  xpcogend  15014  sqrtneglem  15306  rexfiuz  15387  rexanuz2  15389  sumsplit  15805  fsum2dlem  15807  odd2np1  16379  divalgb  16442  gcdcllem2  16538  mrcidb2  17662  fncnvimaeqv  18165  qusecsub  19854  domnmuln0  20710  acsfn1p  20801  lbsacsbs  21159  islpir2  21341  islinds2  21834  islbs4  21853  mplcoe1  22056  mplcoe5  22059  mamucl  22406  mavmulcl  22554  mdetunilem8  22626  iscld4  23074  isconn2  23423  kgencn  23565  tx1cn  23618  tx2cn  23619  elmptrab  23836  isfbas  23838  fbfinnfr  23850  cnfcf  24051  fmucndlem  24301  prdsxmslem2  24543  blval2  24576  cnbl0  24795  cnblcld  24796  metcld  25341  ismbf  25664  ismbfcn  25665  itg1val2  25720  itg2split  25785  itg2monolem1  25786  aannenlem1  26371  pilem1  26496  sinq34lt0t  26552  ellogrn  26602  logeftb  26626  gausslemma2dlem1a  27410  elznns  28389  readdscl  28432  ercgrg  28526  elntg2  29001  usgredgffibi  29342  vtxd0nedgb  29507  vdiscusgrb  29549  upgrspthswlk  29759  s3wwlks2on  29977  clwwlknonwwlknonb  30126  frgrncvvdeqlem2  30320  ch0pss  31465  h1de2ctlem  31575  adjsym  31853  eigposi  31856  dfadj2  31905  elnlfn  31948  xppreima  32656  1stpreima  32717  2ndpreima  32718  creq0  32747  hashgt1  32813  isunit3  33246  isdrng4  33299  qusxpid  33392  lindflbs  33408  dvdsruassoi  33413  dvdsruasso  33414  dvdsrspss  33416  unitprodclb  33418  lsmsnorb  33420  nsgqusf1olem3  33444  qsfld  33527  qtophaus  33836  prsdm  33914  prsrn  33915  1stmbfm  34263  2ndmbfm  34264  eulerpartlemn  34384  reprdifc  34643  circlemeth  34656  bnj1454  34857  bnj984  34967  dffun10  35916  hfext  36185  isfne4b  36343  neifg  36373  taupilem3  37321  topdifinfindis  37348  topdifinffinlem  37349  finxpsuclem  37399  nlpineqsn  37410  wl-ifp-ncond1  37466  poimirlem23  37651  poimirlem26  37654  cnambfre  37676  0totbnd  37781  suceqsneq  38239  opelvvdif  38261  inecmo  38357  brxrn  38376  brin2  38411  eleccossin  38485  dffunsALTV2  38686  dffunsALTV3  38687  dffunsALTV4  38688  elfunsALTV2  38695  elfunsALTV3  38696  elfunsALTV4  38697  elfunsALTV5  38698  dfdisjs2  38711  eldisjs2  38725  disjres  38746  cvrval2  39276  cvrnbtwn2  39277  cvrnbtwn4  39281  hlateq  39402  islpln5  39538  islvol5  39582  pmap11  39765  4atex  40079  cdleme0ex2N  40227  cdlemefrs29pre00  40398  diaord  41050  dihmeetlem13N  41322  lcfl1  41495  lcfls1N  41538  mapdpglem3  41678  isnacs2  42722  mrefg3  42724  pw2f1ocnv  43054  unielss  43235  onmaxnelsup  43240  onsupnmax  43245  onov0suclim  43292  cantnf2  43343  ordsssucb  43353  relexp0eq  43719  frege124d  43779  uneqsn  44043  k0004lem1  44165  sbcoreleleq  44560  modelac8prim  45014  r19.28zf  45169  climreeq  45633  funressnfv  47060  fmtnorec2lem  47534  sclnbgrelself  47839  gpgedgel  48012  eenglngeehlnmlem1  48663  eenglngeehlnmlem2  48664  rrx2linest2  48670  itsclinecirc0b  48700  map0cor  48769  ipolublem  48890  ipoglblem  48893  functermc  49168