Theorem simplbi2com 655

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  elres  5355  xpidtr  5437  elovmpt2rab  6778  elovmpt2rab1  6779  inficl  8214  cfslb2n  8973  repswcshw  13409  cshw1  13419  bezoutlem1  15094  bezoutlem3  15096  modprmn0modprm0  15350  cnprest  20903  haust1  20966  lly1stc  21109  3cyclfrgrarn1  26539  dfon2lem9  30940  phpreu  32563  poimirlem26  32605  sb5ALT  37752  onfrALTlem2  37782  onfrALTlem2VD  38147  sb5ALTVD  38171  funcoressn  39856  ndmaovdistr  39936  reuccatpfxs1  40297  2elfz3nn0  40353  3cyclfrgrrn1  41455