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  1618  necon2abid  2970  reueubd  3363  issetft  3452  reu8  3687  r19.28z  4445  r19.37zv  4449  r19.45zv  4450  r19.44zv  4451  r19.27z  4452  r19.36zv  4454  ralsnsg  4620  eldifvsn  4746  ssunsn2  4776  iunconst  4949  iinconst  4950  iuneqconst  4951  relsng  5740  dmxp  5868  opelres  5933  ordsseleq  6335  ordequn  6411  funssres  6525  fncnv  6554  ffrnbd  6666  fresaun  6694  dff1o5  6772  tz6.12c  6844  funimass4  6886  fndmdifeq0  6977  fneqeql2  6980  unpreima  6996  dffo3  7035  dffo3f  7039  fnnfpeq0  7112  funfvima  7164  f1eqcocnv  7235  fliftf  7249  isocnv3  7266  isomin  7271  eloprabga  7455  mpo2eqb  7478  elpwun  7702  dfom2  7798  opabex3d  7897  opabex3rd  7898  opabex3  7899  f1oweALT  7904  fnwelem  8061  mptsuppd  8117  dfrecs3  8292  oe0m1  8436  oarec  8477  eldifsucnn  8579  naddsuc2  8616  boxcutc  8865  ordunifi  9174  ttrclselem2  9616  r1fin  9666  rankr1c  9714  iscard  9868  iscard2  9869  cardval2  9884  dfac3  10012  kmlem8  10049  infinf  10457  xrlenlt  11177  ltxrlt  11183  negcon2  11414  mulne0b  11758  dfinfre  12103  crne0  12118  elznn  12484  zmax  12843  elfznelfzo  13673  modmuladdnn0  13822  hashneq0  14271  xpcogend  14881  sqrtneglem  15173  rexfiuz  15255  rexanuz2  15257  sumsplit  15675  fsum2dlem  15677  odd2np1  16252  divalgb  16315  gcdcllem2  16411  mrcidb2  17524  fncnvimaeqv  18026  qusecsub  19747  domnmuln0  20624  acsfn1p  20714  lbsacsbs  21093  islpir2  21267  islinds2  21750  islbs4  21769  mplcoe1  21972  mplcoe5  21975  mamucl  22316  mavmulcl  22462  mdetunilem8  22534  iscld4  22980  isconn2  23329  kgencn  23471  tx1cn  23524  tx2cn  23525  elmptrab  23742  isfbas  23744  fbfinnfr  23756  cnfcf  23957  fmucndlem  24205  prdsxmslem2  24444  blval2  24477  cnbl0  24688  cnblcld  24689  metcld  25233  ismbf  25556  ismbfcn  25557  itg1val2  25612  itg2split  25677  itg2monolem1  25678  aannenlem1  26263  pilem1  26388  sinq34lt0t  26445  ellogrn  26495  logeftb  26519  gausslemma2dlem1a  27303  ssltsnb  27732  bdayle  27861  elznns  28326  zsoring  28332  readdscl  28401  ercgrg  28495  elntg2  28963  usgredgffibi  29302  vtxd0nedgb  29467  vdiscusgrb  29509  upgrspthswlk  29716  s3wwlks2on  29934  sps3wwlks2on  29935  clwwlknonwwlknonb  30086  frgrncvvdeqlem2  30280  ch0pss  31425  h1de2ctlem  31535  adjsym  31813  eigposi  31816  dfadj2  31865  elnlfn  31908  xppreima  32627  1stpreima  32688  2ndpreima  32689  creq0  32719  hashgt1  32790  isunit3  33208  isdrng4  33261  qusxpid  33328  lindflbs  33344  dvdsruassoi  33349  dvdsruasso  33350  dvdsrspss  33352  unitprodclb  33354  lsmsnorb  33356  nsgqusf1olem3  33380  qsfld  33463  qtophaus  33849  prsdm  33927  prsrn  33928  1stmbfm  34273  2ndmbfm  34274  eulerpartlemn  34394  reprdifc  34640  circlemeth  34653  bnj1454  34854  bnj984  34964  vonf1owev  35152  dffun10  35956  hfext  36227  isfne4b  36385  neifg  36415  taupilem3  37363  topdifinfindis  37390  topdifinffinlem  37391  finxpsuclem  37441  nlpineqsn  37452  wl-ifp-ncond1  37508  poimirlem23  37693  poimirlem26  37696  cnambfre  37718  0totbnd  37823  opelvvdif  38306  inecmo  38397  brxrn  38417  brin2  38472  suceqsneq  38506  eleccossin  38595  dffunsALTV2  38792  dffunsALTV3  38793  dffunsALTV4  38794  elfunsALTV2  38801  elfunsALTV3  38802  elfunsALTV4  38803  elfunsALTV5  38804  dfdisjs2  38817  eldisjs2  38831  disjres  38852  cvrval2  39383  cvrnbtwn2  39384  cvrnbtwn4  39388  hlateq  39508  islpln5  39644  islvol5  39688  pmap11  39871  4atex  40185  cdleme0ex2N  40333  cdlemefrs29pre00  40504  diaord  41156  dihmeetlem13N  41428  lcfl1  41601  lcfls1N  41644  mapdpglem3  41784  isnacs2  42809  mrefg3  42811  pw2f1ocnv  43140  unielss  43321  onmaxnelsup  43326  onsupnmax  43331  onov0suclim  43377  cantnf2  43428  ordsssucb  43438  relexp0eq  43804  frege124d  43864  uneqsn  44128  k0004lem1  44250  sbcoreleleq  44638  modelac8prim  45095  r19.28zf  45266  climreeq  45723  funressnfv  47153  fmtnorec2lem  47652  sclnbgrelself  47958  gpgiedgdmel  48159  gpgedgel  48160  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  rrx2linest2  48855  itsclinecirc0b  48885  map0cor  48965  ipolublem  49096  ipoglblem  49099  functermc  49619