Theorem bitr4id 293

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 227	. 2 ⊢ (𝜒 ↔ 𝜓)
4	1, 3	bitr2di 291	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  baib  545  cad1  1650  necon2abid  3002  reueubd  3388  issetft  3473  reu8  3698  r19.28z  4465  r19.37zv  4470  r19.45zv  4471  r19.44zv  4472  r19.27z  4473  r19.36zv  4475  ralsnsg  4638  eldifvsn  4767  ssunsn2  4795  iunconst  4968  iinconst  4969  iuneqconst  4970  relsng  5790  dmxp  5921  opelres  5986  ordsseleq  6394  ordequn  6470  funssres  6584  fncnv  6613  ffrnbd  6725  fresaun  6753  dff1o5  6834  tz6.12c  6907  funimass4  6949  fndmdifeq0  7043  fneqeql2  7046  unpreima  7062  dffo3  7101  dffo3f  7105  fnnfpeq0  7182  funfvima  7235  f1eqcocnv  7308  fliftf  7322  isocnv3  7339  isomin  7344  eloprabga  7528  mpo2eqb  7551  elpwun  7774  dfom2  7870  opabex3d  7968  opabex3rd  7969  opabex3  7970  f1oweALT  7975  fnwelem  8133  mptsuppd  8189  dfrecs3  8365  oe0m1  8512  oarec  8553  eldifsucnn  8656  naddsuc2  8694  boxcutc  8945  ordunifi  9257  ttrclselem2  9702  r1fin  9752  rankr1c  9800  iscard  9977  iscard2  9978  cardval2  9993  dfac3  10121  kmlem8  10157  xrlenlt  11291  ltxrlt  11297  negcon2  11528  mulne0b  11872  dfinfre  12213  crne0  12228  elznn  12624  zmax  12987  elfznelfzo  13821  modmuladdnn0  13971  hashneq0  14420  xpcogend  15037  sqrtneglem  15343  rexfiuz  15425  rexanuz2  15427  sumsplit  15844  fsum2dlem  15846  odd2np1  16423  divalgb  16486  gcdcllem2  16582  mrcidb2  17698  fncnvimaeqv  18200  qusxpid  19297  qusecsub  19951  domnmuln0  20860  isdrng4  20891  acsfn1p  20954  lbsacsbs  21332  isfieldidl2  21439  islpir2  21550  islinds2  22015  islbs4  22034  mplcoe1  22240  mplcoe5  22243  mamucl  22610  mavmulcl  22756  mdetunilem8  22828  iscld4  23274  isconn2  23623  kgencn  23766  tx1cn  23819  tx2cn  23820  elmptrab  24037  isfbas  24039  fbfinnfr  24051  cnfcf  24252  fmucndlem  24500  prdsxmslem2  24739  blval2  24772  cnbl0  24983  cnblcld  24984  metcld  25518  ismbf  25840  ismbfcn  25841  itg1val2  25896  itg2split  25961  itg2monolem1  25962  aannenlem1  26544  pilem1  26667  sinq34lt0t  26727  ellogrn  26777  logeftb  26801  gausslemma2dlem1a  27582  sltssnb  28015  bdayle  28162  elznns  28648  zsoring  28655  readdscl  28745  ercgrg  28839  elntg2  29392  usgredgffibi  29734  vtxd0nedgb  29898  vdiscusgrb  29940  upgrspthswlk  30153  s3wwlks2on  30374  sps3wwlks2on  30375  clwwlknonwwlknonb  30526  frgrncvvdeqlem2  30724  ch0pss  31870  h1de2ctlem  31980  adjsym  32258  eigposi  32261  dfadj2  32310  elnlfn  32353  xppreima  33063  1stpreima  33125  2ndpreima  33126  creq0  33153  hashgt1  33225  isunit3  33626  rlocisunit  33662  lindflbs  33758  dvdsruassoi  33763  dvdsruasso  33764  dvdsrspss  33766  unitprodclb  33768  lsmsnorb  33770  nsgqusf1olem3  33790  qsfld  33846  esplyind  34031  qtophaus  34292  prsdm  34370  prsrn  34371  1stmbfm  34717  2ndmbfm  34718  eulerpartlemn  34838  reprdifc  35081  circlemeth  35094  bnj1454  35297  bnj984  35407  vonf1wev  35651  vonf1owevOLD  35653  dffun10  36443  hfext  36714  isfne4b  36911  neifg  36941  taupilem3  38022  topdifinfindis  38051  topdifinffinlem  38052  finxpsuclem  38102  nlpineqsn  38113  wl-ifp-ncond1  38169  poimirlem23  38353  poimirlem26  38356  cnambfre  38378  0totbnd  38484  opelvvdif  38973  inecmo  39064  brxrn  39092  brin2  39147  suceqsneq  39193  eleccossin  39282  dffunsALTV2  39478  dffunsALTV3  39479  dffunsALTV4  39480  elfunsALTV2  39487  elfunsALTV3  39488  elfunsALTV4  39489  elfunsALTV5  39490  dfdisjs2  39503  eldisjs2  39529  disjres  39553  cvrval2  40108  cvrnbtwn2  40109  cvrnbtwn4  40113  hlateq  40233  islpln5  40369  islvol5  40413  pmap11  40596  4atex  40910  cdleme0ex2N  41058  cdlemefrs29pre00  41229  diaord  41881  dihmeetlem13N  42153  lcfl1  42326  lcfls1N  42369  mapdpglem3  42509  isnacs2  43497  mrefg3  43499  pw2f1ocnv  43824  unielss  44005  onmaxnelsup  44010  onsupnmax  44015  onov0suclim  44061  cantnf2  44112  ordsssucb  44122  relexp0eq  44487  frege124d  44547  uneqsn  44811  k0004lem1  44933  sbcoreleleq  45304  modelac8prim  45761  r19.28zf  45937  climreeq  46389  funressnfv  47840  2timesltsqm1  48176  fmtnorec2lem  48354  sclnbgrelself  48673  gpgiedgdmel  48874  gpgedgel  48875  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2linest2  49583  itsclinecirc0b  49613  map0cor  49692  ipolublem  49823  ipoglblem  49826  functermc  50345