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  6120  elovmporab  7664  elovmporab1w  7665  elovmporab1  7666  inficl  9399  cfslb2n  10274  repswcshw  14887  cshw1  14897  bezoutlem1  16635  bezoutlem3  16637  modprmn0modprm0  16905  insubm  18933  cnprest  23520  haust1  23583  lly1stc  23728  3cyclfrgrrn1  30773  dfon2lem9  36376  bj-axreprepsep  37828  phpreu  38366  poimirlem26  38403  eldisjs6  39696  sb5ALT  45356  onfrALTlem2  45377  onfrALTlem2VD  45719  sb5ALTVD  45743  pwclaxpow  45815  funcoressn  47938  ndmaovdistr  48103  2elfz3nn0  48212