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  6073  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  inficl  9316  cfslb2n  10166  repswcshw  14721  cshw1  14731  bezoutlem1  16452  bezoutlem3  16454  modprmn0modprm0  16721  insubm  18728  cnprest  23205  haust1  23268  lly1stc  23412  3cyclfrgrrn1  30267  dfon2lem9  35854  phpreu  37664  poimirlem26  37706  sb5ALT  44642  onfrALTlem2  44663  onfrALTlem2VD  45005  sb5ALTVD  45029  pwclaxpow  45101  funcoressn  47166  ndmaovdistr  47331  2elfz3nn0  47440