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  1649  necon2abid  2997  reueubd  3382  issetft  3466  reu8  3690  r19.28z  4457  r19.37zv  4462  r19.45zv  4463  r19.44zv  4464  r19.27z  4465  r19.36zv  4467  ralsnsg  4630  eldifvsn  4759  ssunsn2  4787  iunconst  4960  iinconst  4961  iuneqconst  4962  relsng  5778  dmxp  5910  opelres  5975  ordsseleq  6392  ordequn  6468  funssres  6584  fncnv  6613  ffrnbd  6725  fresaun  6753  dff1o5  6834  tz6.12c  6907  funimass4  6949  fndmdifeq0  7043  fneqeql2  7046  unpreima  7062  dffo3  7102  dffo3f  7106  fnnfpeq0  7183  funfvima  7236  f1eqcocnv  7309  fliftf  7323  isocnv3  7340  isomin  7345  eloprabga  7529  mpo2eqb  7552  elpwun  7783  dfom2  7879  opabex3d  7977  opabex3rd  7978  opabex3  7979  f1oweALT  7984  fnwelem  8143  mptsuppd  8204  dfrecs3  8380  oe0m1  8529  oarec  8570  eldifsucnn  8673  naddsuc2  8711  boxcutc  8969  ordunifi  9281  ttrclselem2  9727  r1fin  9780  rankr1c  9830  iscard  10056  iscard2  10057  cardval2  10072  dfac3  10200  kmlem8  10236  xrlenlt  11374  ltxrlt  11380  negcon2  11611  mulne0b  11957  dfinfre  12298  crne0  12313  elznn  12709  zmax  13072  elfznelfzo  13908  modmuladdnn0  14058  hashneq0  14508  xpcogend  15127  sqrtneglem  15433  rexfiuz  15515  rexanuz2  15517  sumsplit  15934  fsum2dlem  15936  odd2np1  16511  divalgb  16574  gcdcllem2  16670  mrcidb2  17792  fncnvimaeqv  18294  qusxpid  19395  qusecsub  20049  domnmuln0  20961  isdrng4  20992  acsfn1p  21056  lbsacsbs  21434  isfieldidl2  21541  islpir2  21654  islinds2  22119  islbs4  22138  mplcoe1  22346  mplcoe5  22349  mamucl  22716  mavmulcl  22862  mdetunilem8  22934  iscld4  23383  isconn2  23732  kgencn  23875  tx1cn  23928  tx2cn  23929  elmptrab  24146  isfbas  24148  fbfinnfr  24160  cnfcf  24361  fmucndlem  24609  prdsxmslem2  24848  blval2  24881  cnbl0  25092  cnblcld  25093  metcld  25627  ismbf  25949  ismbfcn  25950  itg1val2  26005  itg2split  26070  itg2monolem1  26071  aannenlem1  26655  pilem1  26778  sinq34lt0t  26838  ellogrn  26887  logeftb  26911  gausslemma2dlem1a  27692  sltssnb  28155  bdayle  28302  elznns  28788  zsoring  28795  readdscl  28885  ercgrg  28980  elntg2  29563  usgredgffibi  29905  vtxd0nedgb  30069  vdiscusgrb  30111  upgrspthswlk  30324  s3wwlks2on  30545  sps3wwlks2on  30546  clwwlknonwwlknonb  30697  frgrncvvdeqlem2  30901  ch0pss  32047  h1de2ctlem  32157  adjsym  32435  eigposi  32438  dfadj2  32487  elnlfn  32530  xppreima  33239  1stpreima  33300  2ndpreima  33301  creq0  33328  hashgt1  33400  isunit3  33801  rlocisunit  33837  lindflbs  33934  dvdsruassoi  33939  dvdsruasso  33940  dvdsrspss  33942  unitprodclb  33944  lsmsnorb  33946  nsgqusf1olem3  33966  qsfld  34022  esplyind  34207  qtophaus  34468  prsdm  34546  prsrn  34547  1stmbfm  34892  2ndmbfm  34893  eulerpartlemn  35013  reprdifc  35256  circlemeth  35269  bnj1454  35472  bnj984  35582  vonf1wev  35887  vonf1owevOLD  35889  dffun10  36676  hfext  36934  isfne4b  37129  neifg  37159  coi1in  37961  taupilem3  38241  topdifinfindis  38270  topdifinffinlem  38271  finxpsuclem  38321  nlpineqsn  38332  wl-ifp-ncond1  38388  poimirlem23  38562  poimirlem26  38565  cnambfre  38587  0totbnd  38708  opelvvdif  39197  inecmo  39288  brxrn  39316  brin2  39371  suceqsneq  39417  eleccossin  39506  dffunsALTV2  39702  dffunsALTV3  39703  dffunsALTV4  39704  elfunsALTV2  39711  elfunsALTV3  39712  elfunsALTV4  39713  elfunsALTV5  39714  dfdisjs2  39727  eldisjs2  39753  disjres  39777  cvrval2  40332  cvrnbtwn2  40333  cvrnbtwn4  40337  hlateq  40457  islpln5  40593  islvol5  40637  pmap11  40820  4atex  41134  cdleme0ex2N  41282  cdlemefrs29pre00  41453  diaord  42105  dihmeetlem13N  42377  lcfl1  42550  lcfls1N  42593  mapdpglem3  42733  isnacs2  43717  mrefg3  43719  pw2f1ocnv  44044  unielss  44220  onmaxnelsup  44225  onsupnmax  44230  onov0suclim  44276  cantnf2  44327  ordsssucb  44337  relexp0eq  44701  frege124d  44761  uneqsn  45025  k0004lem1  45147  sbcoreleleq  45518  modelac8prim  45982  r19.28zf  46174  climreeq  46625  funressnfv  48113  2timesltsqm1  48449  fmtnorec2lem  48627  sclnbgrelself  48946  gpgiedgdmel  49147  gpgedgel  49148  eenglngeehlnmlem1  49849  eenglngeehlnmlem2  49850  rrx2linest2  49856  itsclinecirc0b  49886  map0cor  49965  ipolublem  50094  ipoglblem  50097  functermc  50616