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  6085  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  inficl  9338  cfslb2n  10190  repswcshw  14774  cshw1  14784  bezoutlem1  16508  bezoutlem3  16510  modprmn0modprm0  16778  insubm  18786  cnprest  23254  haust1  23317  lly1stc  23461  3cyclfrgrrn1  30355  dfon2lem9  35971  bj-axreprepsep  37382  phpreu  37925  poimirlem26  37967  eldisjs6  39261  sb5ALT  44952  onfrALTlem2  44973  onfrALTlem2VD  45315  sb5ALTVD  45339  pwclaxpow  45411  funcoressn  47490  ndmaovdistr  47655  2elfz3nn0  47764