Theorem simplbi2com 506

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  xpidtr  5949  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  inficl  8873  cfslb2n  9679  repswcshw  14165  cshw1  14175  bezoutlem1  15877  bezoutlem3  15879  modprmn0modprm0  16134  insubm  17975  cnprest  21894  haust1  21957  lly1stc  22101  3cyclfrgrrn1  28070  dfon2lem9  33149  phpreu  35041  poimirlem26  35083  sb5ALT  41231  onfrALTlem2  41252  onfrALTlem2VD  41595  sb5ALTVD  41619  funcoressn  43634  ndmaovdistr  43763  2elfz3nn0  43873