Theorem simplbiim 659

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  invdisjrab  4671  solin  5087  xpidtr  5553  elpredim  5730  mpt2difsnif  6795  ixpn0  7982  zltaddlt1le  12362  oddnn02np1  15119  sumeven  15157  dvdsprmpweqnn  15636  sgrpass  17337  zringndrg  19886  pmatcoe1fsupp  20554  t1sncld  21178  regsep  21186  nrmsep3  21207  ncvsprp  22998  ncvsm1  23000  ncvsdif  23001  ncvspi  23002  ncvspds  23007  lgsqrlem4  25119  vtxdginducedm1lem4  26494  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  0spth  27104  eucrctshift  27221  frcond1  27246  2pthfrgr  27264  frgrncvvdeqlem7  27285  frgrncvvdeq  27289  frgrwopreglem3  27294  frgrwopreglem5lem  27300  frgr2wwlk1  27309  numclwlk1lem2f1  27347  stcltr1i  29261  bnj570  31101  bnj1145  31187  bnj1398  31228  bnj1442  31243  sconnpht  31337  poimirlem25  33564  2reu1  41507  lighneallem2  41848  fdmdifeqresdif  42445