Theorem simplbi2com 502

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  xpidtr  6154  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  inficl  9494  cfslb2n  10337  repswcshw  14860  cshw1  14870  bezoutlem1  16586  bezoutlem3  16588  modprmn0modprm0  16854  insubm  18853  cnprest  23318  haust1  23381  lly1stc  23525  3cyclfrgrrn1  30317  dfon2lem9  35755  phpreu  37564  poimirlem26  37606  sb5ALT  44496  onfrALTlem2  44517  onfrALTlem2VD  44860  sb5ALTVD  44884  funcoressn  46957  ndmaovdistr  47122  2elfz3nn0  47231