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  6128  elovmporab  7691  elovmporab1w  7692  elovmporab1  7693  inficl  9444  cfslb2n  10373  repswcshw  14991  cshw1  15001  bezoutlem1  16741  bezoutlem3  16743  modprmn0modprm0  17014  insubm  19043  cnprest  23637  haust1  23700  lly1stc  23845  3cyclfrgrrn1  30916  dfon2lem9  36731  bj-axreprepsep  38182  phpreu  38719  poimirlem26  38756  eldisjs6  40064  sb5ALT  45699  onfrALTlem2  45720  onfrALTlem2VD  46062  sb5ALTVD  46086  pwclaxpow  46169  funcoressn  48317  ndmaovdistr  48482  2elfz3nn0  48591