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

This theorem is referenced by:  xpidtr  6142  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  inficl  9465  cfslb2n  10308  repswcshw  14850  cshw1  14860  bezoutlem1  16576  bezoutlem3  16578  modprmn0modprm0  16845  insubm  18831  cnprest  23297  haust1  23360  lly1stc  23504  3cyclfrgrrn1  30304  dfon2lem9  35792  phpreu  37611  poimirlem26  37653  sb5ALT  44545  onfrALTlem2  44566  onfrALTlem2VD  44909  sb5ALTVD  44933  pwclaxpow  45001  funcoressn  47054  ndmaovdistr  47219  2elfz3nn0  47328