Theorem simplbi2com 504

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

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

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 398

This theorem is referenced by:  xpidtr  6067  elovmporab  7582  elovmporab1w  7583  elovmporab1  7584  inficl  9287  cfslb2n  10130  repswcshw  14624  cshw1  14634  bezoutlem1  16347  bezoutlem3  16349  modprmn0modprm0  16606  insubm  18555  cnprest  22546  haust1  22609  lly1stc  22753  3cyclfrgrrn1  28937  dfon2lem9  34050  phpreu  35915  poimirlem26  35957  sb5ALT  42516  onfrALTlem2  42537  onfrALTlem2VD  42880  sb5ALTVD  42904  funcoressn  44952  ndmaovdistr  45115  2elfz3nn0  45224