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  1614  necon2abid  2989  reueubd  3407  issetft  3504  reu8  3755  sbc6gOLD  3835  r19.28z  4521  r19.37zv  4525  r19.45zv  4526  r19.44zv  4527  r19.27z  4528  r19.36zv  4530  ralsnsg  4692  eldifvsn  4822  ssunsn2  4852  iunconst  5024  iinconst  5025  iuneqconst  5026  relsng  5825  dmxp  5953  opelres  6015  ordsseleq  6424  ordequn  6498  funssres  6622  fncnv  6651  ffrnbd  6762  fresaun  6792  dff1o5  6871  tz6.12c  6942  funimass4  6986  fndmdifeq0  7077  fneqeql2  7080  unpreima  7096  dffo3  7136  dffo3f  7140  fnnfpeq0  7212  funfvima  7267  f1eqcocnv  7337  fliftf  7351  isocnv3  7368  isomin  7373  eloprabga  7558  eloprabgaOLD  7559  mpo2eqb  7582  elpwun  7804  dfom2  7905  opabex3d  8006  opabex3rd  8007  opabex3  8008  f1oweALT  8013  fnwelem  8172  mptsuppd  8228  dfrecs3  8428  dfrecs3OLD  8429  oe0m1  8577  oarec  8618  eldifsucnn  8720  naddsuc2  8757  boxcutc  8999  ordunifi  9354  ttrclselem2  9795  r1fin  9842  rankr1c  9890  iscard  10044  iscard2  10045  cardval2  10060  dfac3  10190  kmlem8  10227  infinf  10635  xrlenlt  11355  ltxrlt  11360  negcon2  11589  mulne0b  11931  dfinfre  12276  crne0  12286  elznn  12655  zmax  13010  elfznelfzo  13822  modmuladdnn0  13966  hashneq0  14413  xpcogend  15023  sqrtneglem  15315  rexfiuz  15396  rexanuz2  15398  sumsplit  15816  fsum2dlem  15818  odd2np1  16389  divalgb  16452  gcdcllem2  16546  mrcidb2  17676  fncnvimaeqv  18188  qusecsub  19877  domnmuln0  20731  acsfn1p  20822  lbsacsbs  21181  islpir2  21363  islinds2  21856  islbs4  21875  mplcoe1  22078  mplcoe5  22081  mamucl  22426  mavmulcl  22574  mdetunilem8  22646  iscld4  23094  isconn2  23443  kgencn  23585  tx1cn  23638  tx2cn  23639  elmptrab  23856  isfbas  23858  fbfinnfr  23870  cnfcf  24071  fmucndlem  24321  prdsxmslem2  24563  blval2  24596  cnbl0  24815  cnblcld  24816  metcld  25359  ismbf  25682  ismbfcn  25683  itg1val2  25738  itg2split  25804  itg2monolem1  25805  aannenlem1  26388  pilem1  26513  sinq34lt0t  26569  ellogrn  26619  logeftb  26643  gausslemma2dlem1a  27427  elznns  28406  readdscl  28449  ercgrg  28543  elntg2  29018  usgredgffibi  29359  vtxd0nedgb  29524  vdiscusgrb  29566  upgrspthswlk  29774  s3wwlks2on  29989  clwwlknonwwlknonb  30138  frgrncvvdeqlem2  30332  ch0pss  31477  h1de2ctlem  31587  adjsym  31865  eigposi  31868  dfadj2  31917  elnlfn  31960  xppreima  32664  1stpreima  32718  2ndpreima  32719  creq0  32749  hashgt1  32815  isunit3  33221  isdrng4  33264  qusxpid  33356  lindflbs  33372  dvdsruassoi  33377  dvdsruasso  33378  dvdsrspss  33380  unitprodclb  33382  lsmsnorb  33384  nsgqusf1olem3  33408  qsfld  33491  qtophaus  33782  prsdm  33860  prsrn  33861  1stmbfm  34225  2ndmbfm  34226  eulerpartlemn  34346  reprdifc  34604  circlemeth  34617  bnj1454  34818  bnj984  34928  dffun10  35878  hfext  36147  isfne4b  36307  neifg  36337  taupilem3  37285  topdifinfindis  37312  topdifinffinlem  37313  finxpsuclem  37363  nlpineqsn  37374  wl-ifp-ncond1  37430  poimirlem23  37603  poimirlem26  37606  cnambfre  37628  0totbnd  37733  suceqsneq  38192  opelvvdif  38215  inecmo  38311  brxrn  38330  brin2  38365  eleccossin  38439  dffunsALTV2  38640  dffunsALTV3  38641  dffunsALTV4  38642  elfunsALTV2  38649  elfunsALTV3  38650  elfunsALTV4  38651  elfunsALTV5  38652  dfdisjs2  38665  eldisjs2  38679  disjres  38700  cvrval2  39230  cvrnbtwn2  39231  cvrnbtwn4  39235  hlateq  39356  islpln5  39492  islvol5  39536  pmap11  39719  4atex  40033  cdleme0ex2N  40181  cdlemefrs29pre00  40352  diaord  41004  dihmeetlem13N  41276  lcfl1  41449  lcfls1N  41492  mapdpglem3  41632  isnacs2  42662  mrefg3  42664  pw2f1ocnv  42994  unielss  43179  onmaxnelsup  43184  onsupnmax  43189  onov0suclim  43236  cantnf2  43287  ordsssucb  43297  relexp0eq  43663  frege124d  43723  uneqsn  43987  k0004lem1  44109  sbcoreleleq  44506  r19.28zf  45064  climreeq  45534  funressnfv  46958  fmtnorec2lem  47416  sclnbgrelself  47720  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2linest2  48478  itsclinecirc0b  48508  map0cor  48568  ipolublem  48658  ipoglblem  48661