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  6116  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  inficl  9442  cfslb2n  10287  repswcshw  14835  cshw1  14845  bezoutlem1  16563  bezoutlem3  16565  modprmn0modprm0  16832  insubm  18801  cnprest  23232  haust1  23295  lly1stc  23439  3cyclfrgrrn1  30271  dfon2lem9  35814  phpreu  37633  poimirlem26  37675  sb5ALT  44517  onfrALTlem2  44538  onfrALTlem2VD  44880  sb5ALTVD  44904  pwclaxpow  44976  funcoressn  47038  ndmaovdistr  47203  2elfz3nn0  47312