Theorem simplbi2com 508

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  xpidtr  6127  elovmporab  7669  elovmporab1w  7670  elovmporab1  7671  inficl  9395  cfslb2n  10270  repswcshw  14875  cshw1  14885  bezoutlem1  16622  bezoutlem3  16624  modprmn0modprm0  16892  insubm  18908  cnprest  23483  haust1  23546  lly1stc  23690  3cyclfrgrrn1  30673  dfon2lem9  36302  bj-axreprepsep  37753  phpreu  38296  poimirlem26  38338  eldisjs6  39630  sb5ALT  45275  onfrALTlem2  45296  onfrALTlem2VD  45638  sb5ALTVD  45662  pwclaxpow  45734  funcoressn  47820  ndmaovdistr  47985  2elfz3nn0  48094