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  6115  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  inficl  9420  cfslb2n  10349  repswcshw  14967  cshw1  14977  bezoutlem1  16717  bezoutlem3  16719  modprmn0modprm0  16990  insubm  19019  cnprest  23612  haust1  23675  lly1stc  23820  3cyclfrgrrn1  30891  dfon2lem9  36645  bj-axreprepsep  38083  phpreu  38620  poimirlem26  38657  eldisjs6  39965  sb5ALT  45601  onfrALTlem2  45622  onfrALTlem2VD  45964  sb5ALTVD  45988  pwclaxpow  46067  funcoressn  48205  ndmaovdistr  48370  2elfz3nn0  48479