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  6087  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  inficl  9340  cfslb2n  10190  repswcshw  14747  cshw1  14757  bezoutlem1  16478  bezoutlem3  16480  modprmn0modprm0  16747  insubm  18755  cnprest  23245  haust1  23308  lly1stc  23452  3cyclfrgrrn1  30372  dfon2lem9  36002  bj-axreprepsep  37317  phpreu  37849  poimirlem26  37891  eldisjs6  39185  sb5ALT  44875  onfrALTlem2  44896  onfrALTlem2VD  45238  sb5ALTVD  45262  pwclaxpow  45334  funcoressn  47396  ndmaovdistr  47561  2elfz3nn0  47670