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  6113  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  inficl  9373  cfslb2n  10240  repswcshw  14839  cshw1  14849  bezoutlem1  16587  bezoutlem3  16589  modprmn0modprm0  16857  insubm  18867  cnprest  23407  haust1  23470  lly1stc  23614  3cyclfrgrrn1  30545  dfon2lem9  36152  bj-axreprepsep  37572  phpreu  38115  poimirlem26  38157  eldisjs6  39451  sb5ALT  45099  onfrALTlem2  45120  onfrALTlem2VD  45462  sb5ALTVD  45486  pwclaxpow  45558  funcoressn  47634  ndmaovdistr  47799  2elfz3nn0  47908