Theorem simplbi2com 497

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385

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

This theorem is referenced by:  elresOLD  5646  xpidtr  5736  elovmpt2rab  7114  elovmpt2rab1  7115  inficl  8573  cfslb2n  9378  repswcshw  13897  cshw1  13907  bezoutlem1  15591  bezoutlem3  15593  modprmn0modprm0  15845  cnprest  21422  haust1  21485  lly1stc  21628  3cyclfrgrrn1  27634  dfon2lem9  32208  phpreu  33882  poimirlem26  33924  sb5ALT  39511  onfrALTlem2  39532  onfrALTlem2VD  39885  sb5ALTVD  39909  funcoressn  41925  ndmaovdistr  42061  2elfz3nn0  42166