Theorem simplbi2com 501

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

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

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 395

This theorem is referenced by:  xpidtr  6129  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  inficl  9450  cfslb2n  10293  repswcshw  14798  cshw1  14808  bezoutlem1  16518  bezoutlem3  16520  modprmn0modprm0  16779  insubm  18778  cnprest  23237  haust1  23300  lly1stc  23444  3cyclfrgrrn1  30167  dfon2lem9  35518  phpreu  37208  poimirlem26  37250  sb5ALT  44106  onfrALTlem2  44127  onfrALTlem2VD  44470  sb5ALTVD  44494  funcoressn  46562  ndmaovdistr  46725  2elfz3nn0  46834