Theorem simplbiim 501

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  invdisjrab  4860  solin  5286  xpidtr  5760  elpredim  5932  fvn0ssdmfun  6599  mpt2difsnif  7013  ixpn0  8207  zltaddlt1le  12617  oddnn02np1  15446  sumeven  15484  dvdsprmpweqnn  15960  sgrpass  17643  zringndrg  20198  pmatcoe1fsupp  20876  t1sncld  21501  regsep  21509  nrmsep3  21530  ncvsprp  23321  ncvsm1  23323  ncvsdif  23324  ncvspi  23325  ncvspds  23330  lgsqrlem4  25487  vtxdginducedm1lem4  26840  hashecclwwlkn1  27430  umgrhashecclwwlk  27431  0spth  27502  eucrctshift  27620  frcond1  27647  2pthfrgr  27665  frgrncvvdeqlem7  27686  frgrncvvdeq  27690  frgrwopreglem3  27695  frgrwopreglem5lem  27701  frgr2wwlk1  27710  numclwwlk1lem2f1  27748  numclwwlk1lem2f1OLD  27753  hhcms  28615  stcltr1i  29688  bnj570  31521  bnj1145  31607  bnj1398  31648  bnj1442  31663  sconnpht  31757  poimirlem25  33978  funressnfv  41974  funressnvmo  41976  funressnvmoOLD  41977  2reu1  42011  frnvafv2v  42138  dfatbrafv2b  42147  lighneallem2  42353  fdmdifeqresdif  42967  lindslinindsimp1  43093