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  6122  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  inficl  9447  cfslb2n  10290  repswcshw  14833  cshw1  14843  bezoutlem1  16559  bezoutlem3  16561  modprmn0modprm0  16828  insubm  18801  cnprest  23244  haust1  23307  lly1stc  23451  3cyclfrgrrn1  30233  dfon2lem9  35767  phpreu  37586  poimirlem26  37628  sb5ALT  44517  onfrALTlem2  44538  onfrALTlem2VD  44881  sb5ALTVD  44905  pwclaxpow  44973  funcoressn  47027  ndmaovdistr  47192  2elfz3nn0  47301