Theorem simplbi2com 505

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  xpidtr  5976  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  inficl  8883  cfslb2n  9684  repswcshw  14168  cshw1  14178  bezoutlem1  15881  bezoutlem3  15883  modprmn0modprm0  16138  insubm  17977  cnprest  21891  haust1  21954  lly1stc  22098  3cyclfrgrrn1  28058  dfon2lem9  33031  phpreu  34870  poimirlem26  34912  sb5ALT  40852  onfrALTlem2  40873  onfrALTlem2VD  41216  sb5ALTVD  41240  funcoressn  43271  ndmaovdistr  43400  2elfz3nn0  43510