Theorem simplbi2 383

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 132	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
3	2	ex 114	1 ⊢ (𝜓 → (𝜒 → 𝜑))

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  941  pm5.63dc  942  simplbi2com  1438  reuss2  3408  elni2  7280  elpq  9611  elfz0ubfz0  10085  elfzmlbp  10092  fzo1fzo0n0  10143  elfzo0z  10144  fzofzim  10148  elfzodifsumelfzo  10161  p1modz1  11760  dfgcd2  11973  algcvga  12009  pcprendvds  12248