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  3809  invdisjrab  5039  solin  5493  xpidtr  5987  funimaexg  6466  f1ssres  6623  fvn0ssdmfun  6895  f1veqaeq  7069  f1opw  7461  fprlem1  8041  ixpn0  8611  domunsncan  8745  phplem4  8828  php3  8832  infsupprpr  9120  frrlem15  9373  dfac9  9750  ltxrlt  10903  znegcl  12212  zltaddlt1le  13093  injresinj  13363  fsuppmapnn0fiubex  13565  pfxccatin12lem3  14297  repswswrd  14349  oddnn02np1  15909  sumeven  15948  ncoprmgcdne1b  16207  dvdsprmpweqnn  16438  prmodvdslcmf  16600  sgrpass  18169  symgextf1  18813  fvcosymgeq  18821  ricgic  19766  zringndrg  20455  evlslem4  21034  scmatf1  21428  pmatcoe1fsupp  21598  t1sncld  22223  regsep  22231  nrmsep3  22252  cmpsublem  22296  ufilss  22802  fclscf  22922  ncvsprp  24049  ncvsm1  24051  ncvsdif  24052  ncvspi  24053  ncvspds  24058  mblsplit  24429  mbfdm  24523  fta1glem1  25063  aaliou2  25233  dvloglem  25536  lgsqrlem4  26230  2sqnn0  26319  ausgrusgrb  27256  fusgredgfi  27413  vtxdumgrval  27574  vtxdginducedm1lem4  27630  umgrn1cycl  27891  hashecclwwlkn1  28160  umgrhashecclwwlk  28161  0spth  28209  eucrctshift  28326  frcond1  28349  2pthfrgr  28367  frgrncvvdeqlem7  28388  frgrncvvdeq  28392  frgrwopreglem3  28397  frgrwopreglem5lem  28403  frgr2wwlk1  28412  numclwwlk1lem2f1  28440  hhcms  29284  stcltr1i  30355  bnj570  32598  bnj1145  32686  bnj1398  32727  bnj1442  32742  sconnpht  32904  fmla1  33062  goalrlem  33071  goalr  33072  satfv0fvfmla0  33088  fununiq  33462  rdgprc0  33488  bj-substw  34641  bj-opelresdm  35051  poimirlem25  35539  funressnfv  44209  funressnvmo  44211  euoreqb  44273  frnvafv2v  44400  dfatbrafv2b  44409  prproropf1olem4  44631  lighneallem2  44731  lindslinindsimp1  45471  fullthinc  46000