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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  xpidtr  6123  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  inficl  9424  cfslb2n  10267  repswcshw  14767  cshw1  14777  bezoutlem1  16486  bezoutlem3  16488  modprmn0modprm0  16745  insubm  18736  cnprest  23014  haust1  23077  lly1stc  23221  3cyclfrgrrn1  29806  dfon2lem9  35068  phpreu  36776  poimirlem26  36818  sb5ALT  43589  onfrALTlem2  43610  onfrALTlem2VD  43953  sb5ALTVD  43977  funcoressn  46051  ndmaovdistr  46214  2elfz3nn0  46323