Theorem simplbi2com 657

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  elres  5435  xpidtr  5518  elovmpt2rab  6880  elovmpt2rab1  6881  inficl  8331  cfslb2n  9090  repswcshw  13558  cshw1  13568  bezoutlem1  15256  bezoutlem3  15258  modprmn0modprm0  15512  cnprest  21093  haust1  21156  lly1stc  21299  3cyclfrgrrn1  27149  dfon2lem9  31696  phpreu  33393  poimirlem26  33435  sb5ALT  38731  onfrALTlem2  38761  onfrALTlem2VD  39125  sb5ALTVD  39149  funcoressn  41207  ndmaovdistr  41287  2elfz3nn0  41326  reuccatpfxs1  41434