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  2997  reueubd  3382  issetft  3466  reu8  3691  r19.28z  4458  r19.37zv  4463  r19.45zv  4464  r19.44zv  4465  r19.27z  4466  r19.36zv  4468  ralsnsg  4631  eldifvsn  4760  ssunsn2  4788  iunconst  4961  iinconst  4962  iuneqconst  4963  relsng  5782  dmxp  5913  opelres  5978  ordsseleq  6387  ordequn  6463  funssres  6578  fncnv  6607  ffrnbd  6719  fresaun  6747  dff1o5  6828  tz6.12c  6901  funimass4  6943  fndmdifeq0  7037  fneqeql2  7040  unpreima  7056  dffo3  7096  dffo3f  7100  fnnfpeq0  7177  funfvima  7230  f1eqcocnv  7303  fliftf  7317  isocnv3  7334  isomin  7339  eloprabga  7523  mpo2eqb  7546  elpwun  7769  dfom2  7865  opabex3d  7963  opabex3rd  7964  opabex3  7965  f1oweALT  7970  fnwelem  8130  mptsuppd  8186  dfrecs3  8362  oe0m1  8511  oarec  8552  eldifsucnn  8655  naddsuc2  8693  boxcutc  8951  ordunifi  9263  ttrclselem2  9708  r1fin  9758  rankr1c  9806  iscard  9983  iscard2  9984  cardval2  9999  dfac3  10127  kmlem8  10163  xrlenlt  11301  ltxrlt  11307  negcon2  11538  mulne0b  11882  dfinfre  12223  crne0  12238  elznn  12634  zmax  12997  elfznelfzo  13832  modmuladdnn0  13982  hashneq0  14431  xpcogend  15050  sqrtneglem  15356  rexfiuz  15438  rexanuz2  15440  sumsplit  15857  fsum2dlem  15859  odd2np1  16434  divalgb  16497  gcdcllem2  16593  mrcidb2  17709  fncnvimaeqv  18211  qusxpid  19311  qusecsub  19965  domnmuln0  20874  isdrng4  20905  acsfn1p  20968  lbsacsbs  21346  isfieldidl2  21453  islpir2  21564  islinds2  22029  islbs4  22048  mplcoe1  22256  mplcoe5  22259  mamucl  22626  mavmulcl  22772  mdetunilem8  22844  iscld4  23293  isconn2  23642  kgencn  23785  tx1cn  23838  tx2cn  23839  elmptrab  24056  isfbas  24058  fbfinnfr  24070  cnfcf  24271  fmucndlem  24519  prdsxmslem2  24758  blval2  24791  cnbl0  25002  cnblcld  25003  metcld  25537  ismbf  25859  ismbfcn  25860  itg1val2  25915  itg2split  25980  itg2monolem1  25981  aannenlem1  26567  pilem1  26690  sinq34lt0t  26750  ellogrn  26799  logeftb  26823  gausslemma2dlem1a  27604  sltssnb  28037  bdayle  28184  elznns  28670  zsoring  28677  readdscl  28767  ercgrg  28862  elntg2  29445  usgredgffibi  29787  vtxd0nedgb  29951  vdiscusgrb  29993  upgrspthswlk  30206  s3wwlks2on  30427  sps3wwlks2on  30428  clwwlknonwwlknonb  30579  frgrncvvdeqlem2  30783  ch0pss  31929  h1de2ctlem  32039  adjsym  32317  eigposi  32320  dfadj2  32369  elnlfn  32412  xppreima  33121  1stpreima  33182  2ndpreima  33183  creq0  33210  hashgt1  33282  isunit3  33683  rlocisunit  33719  lindflbs  33815  dvdsruassoi  33820  dvdsruasso  33821  dvdsrspss  33823  unitprodclb  33825  lsmsnorb  33827  nsgqusf1olem3  33847  qsfld  33903  esplyind  34088  qtophaus  34349  prsdm  34427  prsrn  34428  1stmbfm  34774  2ndmbfm  34775  eulerpartlemn  34895  reprdifc  35138  circlemeth  35151  bnj1454  35354  bnj984  35464  vonf1wev  35708  vonf1owevOLD  35710  dffun10  36494  hfext  36766  isfne4b  36963  neifg  36993  taupilem3  38074  topdifinfindis  38103  topdifinffinlem  38104  finxpsuclem  38154  nlpineqsn  38165  wl-ifp-ncond1  38221  poimirlem23  38395  poimirlem26  38398  cnambfre  38420  0totbnd  38526  opelvvdif  39015  inecmo  39106  brxrn  39134  brin2  39189  suceqsneq  39235  eleccossin  39324  dffunsALTV2  39520  dffunsALTV3  39521  dffunsALTV4  39522  elfunsALTV2  39529  elfunsALTV3  39530  elfunsALTV4  39531  elfunsALTV5  39532  dfdisjs2  39545  eldisjs2  39571  disjres  39595  cvrval2  40150  cvrnbtwn2  40151  cvrnbtwn4  40155  hlateq  40275  islpln5  40411  islvol5  40455  pmap11  40638  4atex  40952  cdleme0ex2N  41100  cdlemefrs29pre00  41271  diaord  41923  dihmeetlem13N  42195  lcfl1  42368  lcfls1N  42411  mapdpglem3  42551  isnacs2  43554  mrefg3  43556  pw2f1ocnv  43881  unielss  44062  onmaxnelsup  44067  onsupnmax  44072  onov0suclim  44118  cantnf2  44169  ordsssucb  44179  relexp0eq  44544  frege124d  44604  uneqsn  44868  k0004lem1  44990  sbcoreleleq  45361  modelac8prim  45818  r19.28zf  45994  climreeq  46446  funressnfv  47934  2timesltsqm1  48270  fmtnorec2lem  48448  sclnbgrelself  48767  gpgiedgdmel  48968  gpgedgel  48969  eenglngeehlnmlem1  49670  eenglngeehlnmlem2  49671  rrx2linest2  49677  itsclinecirc0b  49707  map0cor  49786  ipolublem  49915  ipoglblem  49918  functermc  50437