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  6098  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  inficl  9383  cfslb2n  10228  repswcshw  14784  cshw1  14794  bezoutlem1  16516  bezoutlem3  16518  modprmn0modprm0  16785  insubm  18752  cnprest  23183  haust1  23246  lly1stc  23390  3cyclfrgrrn1  30221  dfon2lem9  35786  phpreu  37605  poimirlem26  37647  sb5ALT  44522  onfrALTlem2  44543  onfrALTlem2VD  44885  sb5ALTVD  44909  pwclaxpow  44981  funcoressn  47047  ndmaovdistr  47212  2elfz3nn0  47321