Theorem simplbi2com 503

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

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

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 397

This theorem is referenced by:  xpidtr  6027  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  inficl  9184  cfslb2n  10024  repswcshw  14525  cshw1  14535  bezoutlem1  16247  bezoutlem3  16249  modprmn0modprm0  16508  insubm  18457  cnprest  22440  haust1  22503  lly1stc  22647  3cyclfrgrrn1  28649  dfon2lem9  33767  phpreu  35761  poimirlem26  35803  sb5ALT  42145  onfrALTlem2  42166  onfrALTlem2VD  42509  sb5ALTVD  42533  funcoressn  44536  ndmaovdistr  44699  2elfz3nn0  44808