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  2998  reueubd  3383  issetft  3467  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  5779  dmxp  5911  opelres  5976  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  38240  topdifinfindis  38269  topdifinffinlem  38270  finxpsuclem  38320  nlpineqsn  38331  wl-ifp-ncond1  38387  poimirlem23  38561  poimirlem26  38564  cnambfre  38586  0totbnd  38707  opelvvdif  39196  inecmo  39287  brxrn  39315  brin2  39370  suceqsneq  39416  eleccossin  39505  dffunsALTV2  39701  dffunsALTV3  39702  dffunsALTV4  39703  elfunsALTV2  39710  elfunsALTV3  39711  elfunsALTV4  39712  elfunsALTV5  39713  dfdisjs2  39726  eldisjs2  39752  disjres  39776  cvrval2  40331  cvrnbtwn2  40332  cvrnbtwn4  40336  hlateq  40456  islpln5  40592  islvol5  40636  pmap11  40819  4atex  41133  cdleme0ex2N  41281  cdlemefrs29pre00  41452  diaord  42104  dihmeetlem13N  42376  lcfl1  42549  lcfls1N  42592  mapdpglem3  42732  isnacs2  43716  mrefg3  43718  pw2f1ocnv  44043  unielss  44219  onmaxnelsup  44224  onsupnmax  44229  onov0suclim  44275  cantnf2  44326  ordsssucb  44336  relexp0eq  44700  frege124d  44760  uneqsn  45024  k0004lem1  45146  sbcoreleleq  45517  modelac8prim  45981  r19.28zf  46173  climreeq  46624  funressnfv  48112  2timesltsqm1  48448  fmtnorec2lem  48626  sclnbgrelself  48945  gpgiedgdmel  49146  gpgedgel  49147  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2linest2  49855  itsclinecirc0b  49885  map0cor  49964  ipolublem  50093  ipoglblem  50096  functermc  50615