Theorem simplbi2com 507

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  xpidtr  6124  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  inficl  9386  cfslb2n  10253  repswcshw  14851  cshw1  14861  bezoutlem1  16598  bezoutlem3  16600  modprmn0modprm0  16868  insubm  18878  cnprest  23427  haust1  23490  lly1stc  23634  3cyclfrgrrn1  30614  dfon2lem9  36259  bj-axreprepsep  37690  phpreu  38233  poimirlem26  38275  eldisjs6  39567  sb5ALT  45214  onfrALTlem2  45235  onfrALTlem2VD  45577  sb5ALTVD  45601  pwclaxpow  45673  funcoressn  47756  ndmaovdistr  47921  2elfz3nn0  48030