Theorem simplbiim 507

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  2reu1  3883  invdisjrab  5054  solin  5500  xpidtr  5984  elpredim  6162  funimaexg  6442  f1ssres  6584  fvn0ssdmfun  6844  f1veqaeq  7017  f1opw  7403  ixpn0  8496  domunsncan  8619  phplem4  8701  php3  8705  infsupprpr  8970  dfac9  9564  ltxrlt  10713  znegcl  12020  zltaddlt1le  12893  injresinj  13161  fsuppmapnn0fiubex  13363  pfxccatin12lem3  14096  repswswrd  14148  oddnn02np1  15699  sumeven  15740  ncoprmgcdne1b  15996  dvdsprmpweqnn  16223  prmodvdslcmf  16385  sgrpass  17909  symgextf1  18551  fvcosymgeq  18559  ricgic  19503  evlslem4  20290  zringndrg  20639  scmatf1  21142  pmatcoe1fsupp  21311  t1sncld  21936  regsep  21944  nrmsep3  21965  cmpsublem  22009  ufilss  22515  fclscf  22635  ncvsprp  23758  ncvsm1  23760  ncvsdif  23761  ncvspi  23762  ncvspds  23767  mblsplit  24135  mbfdm  24229  fta1glem1  24761  aaliou2  24931  dvloglem  25233  lgsqrlem4  25927  2sqnn0  26016  ausgrusgrb  26952  fusgredgfi  27109  vtxdumgrval  27270  vtxdginducedm1lem4  27326  umgrn1cycl  27587  hashecclwwlkn1  27858  umgrhashecclwwlk  27859  0spth  27907  eucrctshift  28024  frcond1  28047  2pthfrgr  28065  frgrncvvdeqlem7  28086  frgrncvvdeq  28090  frgrwopreglem3  28095  frgrwopreglem5lem  28101  frgr2wwlk1  28110  numclwwlk1lem2f1  28138  hhcms  28982  stcltr1i  30053  bnj570  32179  bnj1145  32267  bnj1398  32308  bnj1442  32323  sconnpht  32478  fmla1  32636  goalrlem  32645  goalr  32646  satfv0fvfmla0  32662  fununiq  33014  fprlem1  33139  frrlem15  33144  bj-opelresdm  34439  poimirlem25  34919  funressnfv  43285  funressnvmo  43287  euoreqb  43315  frnvafv2v  43442  dfatbrafv2b  43451  prproropf1olem4  43675  lighneallem2  43778  lindslinindsimp1  44519