Theorem simplbi2com 503

Description: A deduction eliminating a conjunct, similar to simplbi2 501. (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 501	. 2 ⊢ (𝜓 → (𝜒 → 𝜑))
3	2	com12 32	1 ⊢ (𝜒 → (𝜓 → 𝜑))

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

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 397

This theorem is referenced by:  xpidtr  6123  elovmporab  7654  elovmporab1w  7655  elovmporab1  7656  inficl  9422  cfslb2n  10265  repswcshw  14764  cshw1  14774  bezoutlem1  16483  bezoutlem3  16485  modprmn0modprm0  16742  insubm  18701  cnprest  22800  haust1  22863  lly1stc  23007  3cyclfrgrrn1  29576  dfon2lem9  34838  phpreu  36564  poimirlem26  36606  sb5ALT  43374  onfrALTlem2  43395  onfrALTlem2VD  43738  sb5ALTVD  43762  funcoressn  45837  ndmaovdistr  46000  2elfz3nn0  46109