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  6095  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  inficl  9376  cfslb2n  10221  repswcshw  14777  cshw1  14787  bezoutlem1  16509  bezoutlem3  16511  modprmn0modprm0  16778  insubm  18745  cnprest  23176  haust1  23239  lly1stc  23383  3cyclfrgrrn1  30214  dfon2lem9  35779  phpreu  37598  poimirlem26  37640  sb5ALT  44515  onfrALTlem2  44536  onfrALTlem2VD  44878  sb5ALTVD  44902  pwclaxpow  44974  funcoressn  47043  ndmaovdistr  47208  2elfz3nn0  47317