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  6114  elovmporab  7659  elovmporab1w  7660  elovmporab1  7661  inficl  9401  cfslb2n  10327  repswcshw  14943  cshw1  14953  bezoutlem1  16692  bezoutlem3  16694  modprmn0modprm0  16965  insubm  18994  cnprest  23587  haust1  23650  lly1stc  23795  3cyclfrgrrn1  30868  dfon2lem9  36523  bj-axreprepsep  37959  phpreu  38495  poimirlem26  38532  eldisjs6  39840  sb5ALT  45467  onfrALTlem2  45488  onfrALTlem2VD  45830  sb5ALTVD  45854  pwclaxpow  45926  funcoressn  48056  ndmaovdistr  48221  2elfz3nn0  48330