Theorem simplbiim 508

Description: Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)

Hypotheses

Ref	Expression
simplbiim.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
simplbiim.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
simplbiim	⊢ (𝜑 → 𝜃)

Proof of Theorem simplbiim

Step	Hyp	Ref	Expression
1		simplbiim.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	simprbi 500	. 2 ⊢ (𝜑 → 𝜒)
3		simplbiim.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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  df-an 400

This theorem is referenced by:  2reu1  3826  invdisjrab  5016  solin  5462  xpidtr  5949  elpredim  6128  funimaexg  6410  f1ssres  6557  fvn0ssdmfun  6819  f1veqaeq  6993  f1opw  7381  ixpn0  8477  domunsncan  8600  phplem4  8683  php3  8687  infsupprpr  8952  dfac9  9547  ltxrlt  10700  znegcl  12005  zltaddlt1le  12883  injresinj  13153  fsuppmapnn0fiubex  13355  pfxccatin12lem3  14085  repswswrd  14137  oddnn02np1  15689  sumeven  15728  ncoprmgcdne1b  15984  dvdsprmpweqnn  16211  prmodvdslcmf  16373  sgrpass  17899  symgextf1  18541  fvcosymgeq  18549  ricgic  19494  zringndrg  20183  evlslem4  20747  scmatf1  21136  pmatcoe1fsupp  21306  t1sncld  21931  regsep  21939  nrmsep3  21960  cmpsublem  22004  ufilss  22510  fclscf  22630  ncvsprp  23757  ncvsm1  23759  ncvsdif  23760  ncvspi  23761  ncvspds  23766  mblsplit  24136  mbfdm  24230  fta1glem1  24766  aaliou2  24936  dvloglem  25239  lgsqrlem4  25933  2sqnn0  26022  ausgrusgrb  26958  fusgredgfi  27115  vtxdumgrval  27276  vtxdginducedm1lem4  27332  umgrn1cycl  27593  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  0spth  27911  eucrctshift  28028  frcond1  28051  2pthfrgr  28069  frgrncvvdeqlem7  28090  frgrncvvdeq  28094  frgrwopreglem3  28099  frgrwopreglem5lem  28105  frgr2wwlk1  28114  numclwwlk1lem2f1  28142  hhcms  28986  stcltr1i  30057  bnj570  32287  bnj1145  32375  bnj1398  32416  bnj1442  32431  sconnpht  32589  fmla1  32747  goalrlem  32756  goalr  32757  satfv0fvfmla0  32773  fununiq  33125  rdgprc0  33151  fprlem1  33250  frrlem15  33255  bj-substw  34169  bj-opelresdm  34560  poimirlem25  35082  funressnfv  43635  funressnvmo  43637  euoreqb  43665  frnvafv2v  43792  dfatbrafv2b  43801  prproropf1olem4  44023  lighneallem2  44124  lindslinindsimp1  44866