Theorem simplbi2com 502

Description: A deduction eliminating a conjunct, similar to simplbi2 500. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.)

Hypothesis

Ref	Expression
simplbi2com.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi2com	⊢ (𝜒 → (𝜓 → 𝜑))

Proof of Theorem simplbi2com

Step	Hyp	Ref	Expression
1		simplbi2com.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	simplbi2 500	. 2 ⊢ (𝜓 → (𝜒 → 𝜑))
3	2	com12 32	1 ⊢ (𝜒 → (𝜓 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  xpidtr  6016  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  inficl  9114  cfslb2n  9955  repswcshw  14453  cshw1  14463  bezoutlem1  16175  bezoutlem3  16177  modprmn0modprm0  16436  insubm  18372  cnprest  22348  haust1  22411  lly1stc  22555  3cyclfrgrrn1  28550  dfon2lem9  33673  phpreu  35688  poimirlem26  35730  sb5ALT  42034  onfrALTlem2  42055  onfrALTlem2VD  42398  sb5ALTVD  42422  funcoressn  44423  ndmaovdistr  44586  2elfz3nn0  44696