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  6069  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  inficl  9309  cfslb2n  10156  repswcshw  14716  cshw1  14726  bezoutlem1  16447  bezoutlem3  16449  modprmn0modprm0  16716  insubm  18723  cnprest  23202  haust1  23265  lly1stc  23409  3cyclfrgrrn1  30260  dfon2lem9  35824  phpreu  37643  poimirlem26  37685  sb5ALT  44557  onfrALTlem2  44578  onfrALTlem2VD  44920  sb5ALTVD  44944  pwclaxpow  45016  funcoressn  47072  ndmaovdistr  47237  2elfz3nn0  47346