Theorem simplbi2com 503

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  xpidtr  6079  elovmporab  7609  elovmporab1w  7610  elovmporab1  7611  inficl  9335  cfslb2n  10188  repswcshw  14772  cshw1  14782  bezoutlem1  16506  bezoutlem3  16508  modprmn0modprm0  16776  insubm  18784  cnprest  23279  haust1  23342  lly1stc  23486  3cyclfrgrrn1  30380  dfon2lem9  36024  bj-axreprepsep  37435  phpreu  37978  poimirlem26  38020  eldisjs6  39314  sb5ALT  44976  onfrALTlem2  44997  onfrALTlem2VD  45339  sb5ALTVD  45363  pwclaxpow  45435  funcoressn  47512  ndmaovdistr  47677  2elfz3nn0  47786