Theorem simplbiim 505

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 497	. 2 ⊢ (𝜑 → 𝜒)
3		simplbiim.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  2reu1  3891  invdisjrab  5134  solin  5613  xpidtr  6123  funimaexgOLD  6635  f1ssres  6795  fvn0ssdmfun  7076  f1veqaeq  7258  f1opw  7664  fprlem1  8287  ixpn0  8926  domunsncan  9074  phplem2  9210  php3  9214  phplem4OLD  9222  php3OLD  9226  infsupprpr  9501  frrlem15  9754  dfac9  10133  ltxrlt  11286  znegcl  12599  zltaddlt1le  13484  injresinj  13755  fsuppmapnn0fiubex  13959  pfxccatin12lem3  14684  repswswrd  14736  oddnn02np1  16293  sumeven  16332  ncoprmgcdne1b  16589  dvdsprmpweqnn  16820  prmodvdslcmf  16982  sgrpass  18618  symgextf1  19291  fvcosymgeq  19299  ricgic  20290  zringndrg  21044  evlslem4  21643  scmatf1  22040  pmatcoe1fsupp  22210  t1sncld  22837  regsep  22845  nrmsep3  22866  cmpsublem  22910  ufilss  23416  fclscf  23536  ncvsprp  24676  ncvsm1  24678  ncvsdif  24679  ncvspi  24680  ncvspds  24685  mblsplit  25056  mbfdm  25150  fta1glem1  25690  aaliou2  25860  dvloglem  26163  lgsqrlem4  26859  2sqnn0  26948  ausgrusgrb  28463  fusgredgfi  28620  vtxdumgrval  28781  vtxdginducedm1lem4  28837  umgrn1cycl  29099  hashecclwwlkn1  29368  umgrhashecclwwlk  29369  0spth  29417  eucrctshift  29534  frcond1  29557  2pthfrgr  29575  frgrncvvdeqlem7  29596  frgrncvvdeq  29600  frgrwopreglem3  29605  frgrwopreglem5lem  29611  frgr2wwlk1  29620  numclwwlk1lem2f1  29648  hhcms  30494  stcltr1i  31565  bnj570  33985  bnj1145  34073  bnj1398  34114  bnj1442  34129  sconnpht  34289  fmla1  34447  goalrlem  34456  goalr  34457  satfv0fvfmla0  34473  fununiq  34809  rdgprc0  34834  bj-substw  35686  bj-opelresdm  36112  poimirlem25  36599  funressnfv  45832  funressnvmo  45834  euoreqb  45896  fcdmvafv2v  46023  dfatbrafv2b  46032  prproropf1olem4  46253  lighneallem2  46353  lindslinindsimp1  47216  fullthinc  47744