Theorem simplbi2com 506

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  xpidtr  6106  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  inficl  9368  cfslb2n  10222  repswcshw  14822  cshw1  14832  bezoutlem1  16556  bezoutlem3  16558  modprmn0modprm0  16826  insubm  18835  cnprest  23329  haust1  23392  lly1stc  23536  3cyclfrgrrn1  30433  dfon2lem9  36103  bj-axreprepsep  37524  phpreu  38067  poimirlem26  38109  eldisjs6  39403  sb5ALT  45065  onfrALTlem2  45086  onfrALTlem2VD  45428  sb5ALTVD  45452  pwclaxpow  45524  funcoressn  47600  ndmaovdistr  47765  2elfz3nn0  47874