Theorem simplbi2com 507

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  xpidtr  6112  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  inficl  9373  cfslb2n  10240  repswcshw  14837  cshw1  14847  bezoutlem1  16585  bezoutlem3  16587  modprmn0modprm0  16855  insubm  18865  cnprest  23403  haust1  23466  lly1stc  23610  3cyclfrgrrn1  30541  dfon2lem9  36147  bj-axreprepsep  37567  phpreu  38110  poimirlem26  38152  eldisjs6  39446  sb5ALT  45093  onfrALTlem2  45114  onfrALTlem2VD  45456  sb5ALTVD  45480  pwclaxpow  45552  funcoressn  47635  ndmaovdistr  47800  2elfz3nn0  47909