Theorem simplbi2 385

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
pm3.26bi2.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi2	⊢ (𝜓 → (𝜒 → 𝜑))

Proof of Theorem simplbi2

Step	Hyp	Ref	Expression
1		pm3.26bi2.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpri 133	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 115	1 ⊢ (𝜓 → (𝜒 → 𝜑))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.62dc  951  pm5.63dc  952  simplbi2com  1487  reuss2  3484  elni2  7509  elpq  9852  elfz0ubfz0  10329  elfzmlbp  10336  fzo1fzo0n0  10391  elfzo0z  10392  fzofzim  10396  elfzodifsumelfzo  10415  swrdswrd  11245  swrdccatin1  11265  p1modz1  12313  dfgcd2  12543  algcvga  12581  pcprendvds  12821  usgruspgrben  15992  trlf1  16106