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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  baib  544  cad1  1647  necon2abid  3000  reueubd  3386  issetft  3471  reu8  3696  r19.28z  4463  r19.37zv  4468  r19.45zv  4469  r19.44zv  4470  r19.27z  4471  r19.36zv  4473  ralsnsg  4636  eldifvsn  4765  ssunsn2  4793  iunconst  4966  iinconst  4967  iuneqconst  4968  relsng  5788  dmxp  5919  opelres  5984  ordsseleq  6390  ordequn  6466  funssres  6580  fncnv  6609  ffrnbd  6721  fresaun  6749  dff1o5  6830  tz6.12c  6903  funimass4  6945  fndmdifeq0  7039  fneqeql2  7042  unpreima  7058  dffo3  7097  dffo3f  7101  fnnfpeq0  7176  funfvima  7228  f1eqcocnv  7299  fliftf  7313  isocnv3  7330  isomin  7335  eloprabga  7519  mpo2eqb  7542  elpwun  7764  dfom2  7860  opabex3d  7958  opabex3rd  7959  opabex3  7960  f1oweALT  7965  fnwelem  8123  mptsuppd  8179  dfrecs3  8355  oe0m1  8502  oarec  8543  eldifsucnn  8646  naddsuc2  8684  boxcutc  8935  ordunifi  9246  ttrclselem2  9691  r1fin  9741  rankr1c  9789  iscard  9957  iscard2  9958  cardval2  9973  dfac3  10101  kmlem8  10137  xrlenlt  11269  ltxrlt  11275  negcon2  11506  mulne0b  11850  dfinfre  12191  crne0  12206  elznn  12602  zmax  12964  elfznelfzo  13798  modmuladdnn0  13947  hashneq0  14396  xpcogend  15007  sqrtneglem  15313  rexfiuz  15395  rexanuz2  15397  sumsplit  15815  fsum2dlem  15817  odd2np1  16394  divalgb  16457  gcdcllem2  16553  mrcidb2  17669  fncnvimaeqv  18171  qusxpid  19246  qusecsub  19900  domnmuln0  20808  isdrng4  20839  acsfn1p  20902  lbsacsbs  21280  isfieldidl2  21387  islpir2  21498  islinds2  21963  islbs4  21982  mplcoe1  22188  mplcoe5  22191  mamucl  22558  mavmulcl  22704  mdetunilem8  22776  iscld4  23222  isconn2  23571  kgencn  23713  tx1cn  23766  tx2cn  23767  elmptrab  23984  isfbas  23986  fbfinnfr  23998  cnfcf  24199  fmucndlem  24447  prdsxmslem2  24686  blval2  24719  cnbl0  24930  cnblcld  24931  metcld  25465  ismbf  25787  ismbfcn  25788  itg1val2  25843  itg2split  25908  itg2monolem1  25909  aannenlem1  26491  pilem1  26614  sinq34lt0t  26674  ellogrn  26724  logeftb  26748  gausslemma2dlem1a  27529  sltssnb  27962  bdayle  28109  elznns  28595  zsoring  28602  readdscl  28692  ercgrg  28786  elntg2  29335  usgredgffibi  29674  vtxd0nedgb  29838  vdiscusgrb  29880  upgrspthswlk  30087  s3wwlks2on  30305  sps3wwlks2on  30306  clwwlknonwwlknonb  30457  frgrncvvdeqlem2  30651  ch0pss  31797  h1de2ctlem  31907  adjsym  32185  eigposi  32188  dfadj2  32237  elnlfn  32280  xppreima  32990  1stpreima  33052  2ndpreima  33053  creq0  33081  hashgt1  33153  isunit3  33560  rlocisunit  33596  lindflbs  33692  dvdsruassoi  33697  dvdsruasso  33698  dvdsrspss  33700  unitprodclb  33702  lsmsnorb  33704  nsgqusf1olem3  33724  qsfld  33780  esplyind  33965  qtophaus  34226  prsdm  34304  prsrn  34305  1stmbfm  34650  2ndmbfm  34651  eulerpartlemn  34771  reprdifc  35014  circlemeth  35027  bnj1454  35230  bnj984  35340  vonf1wev  35592  vonf1owevOLD  35594  dffun10  36404  hfext  36675  isfne4b  36872  neifg  36902  taupilem3  37983  topdifinfindis  38012  topdifinffinlem  38013  finxpsuclem  38063  nlpineqsn  38074  wl-ifp-ncond1  38130  poimirlem23  38314  poimirlem26  38317  cnambfre  38339  0totbnd  38444  opelvvdif  38933  inecmo  39024  brxrn  39052  brin2  39107  suceqsneq  39153  eleccossin  39242  dffunsALTV2  39438  dffunsALTV3  39439  dffunsALTV4  39440  elfunsALTV2  39447  elfunsALTV3  39448  elfunsALTV4  39449  elfunsALTV5  39450  dfdisjs2  39463  eldisjs2  39489  disjres  39513  cvrval2  40068  cvrnbtwn2  40069  cvrnbtwn4  40073  hlateq  40193  islpln5  40329  islvol5  40373  pmap11  40556  4atex  40870  cdleme0ex2N  41018  cdlemefrs29pre00  41189  diaord  41841  dihmeetlem13N  42113  lcfl1  42286  lcfls1N  42329  mapdpglem3  42469  isnacs2  43457  mrefg3  43459  pw2f1ocnv  43784  unielss  43965  onmaxnelsup  43970  onsupnmax  43975  onov0suclim  44021  cantnf2  44072  ordsssucb  44082  relexp0eq  44447  frege124d  44507  uneqsn  44771  k0004lem1  44893  sbcoreleleq  45264  modelac8prim  45721  r19.28zf  45897  climreeq  46349  funressnfv  47800  2timesltsqm1  48136  fmtnorec2lem  48314  sclnbgrelself  48633  gpgiedgdmel  48834  gpgedgel  48835  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2linest2  49544  itsclinecirc0b  49574  map0cor  49653  ipolublem  49784  ipoglblem  49787  functermc  50306