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  6075  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  inficl  9334  cfslb2n  10181  repswcshw  14736  cshw1  14746  bezoutlem1  16468  bezoutlem3  16470  modprmn0modprm0  16737  insubm  18710  cnprest  23192  haust1  23255  lly1stc  23399  3cyclfrgrrn1  30247  dfon2lem9  35764  phpreu  37583  poimirlem26  37625  sb5ALT  44499  onfrALTlem2  44520  onfrALTlem2VD  44862  sb5ALTVD  44886  pwclaxpow  44958  funcoressn  47027  ndmaovdistr  47192  2elfz3nn0  47301