Theorem simplbiim 657

Description: Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
simplbiim.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
simplbiim.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
simplbiim	⊢ (𝜑 → 𝜃)

Proof of Theorem simplbiim

Step	Hyp	Ref	Expression
1		simplbiim.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		simplbiim.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	adantl 481	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 206	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385

This theorem is referenced by:  invdisjrab  4572  solin  4982  xpidtr  5437  elpredim  5609  zltaddlt1le  12195  oddnn02np1  14910  sumeven  14948  dvdsprmpweqnn  15427  zringndrg  19657  pmatcoe1fsupp  20325  ncvsprp  22760  ncvsm1  22762  ncvsdif  22763  ncvspi  22764  ncvspds  22769  lgsqrlem4  24874  bnj570  30229  bnj1145  30315  bnj1398  30356  bnj1442  30371  poimirlem25  32604  lighneallem2  40061  isclwwlksnx  41197  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  eucrctshift  41411  2pthfrgr  41454  frgrncvvdeqlem3  41471  frgrncvvdeqlemA  41476  frgrncvvdeq  41480  frgr2wwlk1  41494  frgr2wwlkeqm  41496