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  6079  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  inficl  9331  cfslb2n  10181  repswcshw  14765  cshw1  14775  bezoutlem1  16499  bezoutlem3  16501  modprmn0modprm0  16769  insubm  18777  cnprest  23264  haust1  23327  lly1stc  23471  3cyclfrgrrn1  30370  dfon2lem9  35987  bj-axreprepsep  37398  phpreu  37939  poimirlem26  37981  eldisjs6  39275  sb5ALT  44970  onfrALTlem2  44991  onfrALTlem2VD  45333  sb5ALTVD  45357  pwclaxpow  45429  funcoressn  47502  ndmaovdistr  47667  2elfz3nn0  47776