Theorem simplbi2com 498

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

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

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 387

This theorem is referenced by:  elresOLD  5672  xpidtr  5760  elovmpt2rab  7140  elovmpt2rab1  7141  inficl  8600  cfslb2n  9405  repswcshw  13933  cshw1  13943  bezoutlem1  15629  bezoutlem3  15631  modprmn0modprm0  15883  cnprest  21464  haust1  21527  lly1stc  21670  3cyclfrgrrn1  27666  dfon2lem9  32234  phpreu  33936  poimirlem26  33979  sb5ALT  39569  onfrALTlem2  39590  onfrALTlem2VD  39943  sb5ALTVD  39967  funcoressn  41973  ndmaovdistr  42109  2elfz3nn0  42214