Theorem simplbi2com 503

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  xpidtr  6123  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  inficl  9419  cfslb2n  10262  repswcshw  14761  cshw1  14771  bezoutlem1  16480  bezoutlem3  16482  modprmn0modprm0  16739  insubm  18698  cnprest  22792  haust1  22855  lly1stc  22999  3cyclfrgrrn1  29535  dfon2lem9  34758  phpreu  36467  poimirlem26  36509  sb5ALT  43276  onfrALTlem2  43297  onfrALTlem2VD  43640  sb5ALTVD  43664  funcoressn  45742  ndmaovdistr  45905  2elfz3nn0  46014