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  6079  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  inficl  9328  cfslb2n  10178  repswcshw  14735  cshw1  14745  bezoutlem1  16466  bezoutlem3  16468  modprmn0modprm0  16735  insubm  18743  cnprest  23233  haust1  23296  lly1stc  23440  3cyclfrgrrn1  30360  dfon2lem9  35983  phpreu  37801  poimirlem26  37843  sb5ALT  44762  onfrALTlem2  44783  onfrALTlem2VD  45125  sb5ALTVD  45149  pwclaxpow  45221  funcoressn  47284  ndmaovdistr  47449  2elfz3nn0  47558