Theorem simplbiim 659

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 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 3	sylbi 207	1 ⊢ (𝜑 → 𝜃)

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

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 386

This theorem is referenced by:  invdisjrab  4639  solin  5058  xpidtr  5518  elpredim  5692  mpt2difsnif  6753  ixpn0  7940  zltaddlt1le  12324  oddnn02np1  15072  sumeven  15110  dvdsprmpweqnn  15589  sgrpass  17290  zringndrg  19838  pmatcoe1fsupp  20506  t1sncld  21130  regsep  21138  nrmsep3  21159  ncvsprp  22952  ncvsm1  22954  ncvsdif  22955  ncvspi  22956  ncvspds  22961  lgsqrlem4  25074  vtxdginducedm1lem4  26438  isclwwlksnx  26889  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  0spth  26987  eucrctshift  27103  frcond1  27130  2pthfrgr  27148  frgrncvvdeqlem7  27169  frgrncvvdeq  27173  frgrwopreglem3  27178  frgrwopreglem5lem  27184  frgr2wwlk1  27193  stcltr1i  29133  bnj570  30975  bnj1145  31061  bnj1398  31102  bnj1442  31117  sconnpht  31211  poimirlem25  33434  2reu1  41186  lighneallem2  41523  fdmdifeqresdif  42120