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 ⊢ (𝜓 → (𝜒 → 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.62dc  958  pm5.63dc  959  simplbi2com  1494  reuss2  3513  elni2  7681  elpq  10051  elfz0ubfz0  10534  elfzmlbp  10541  fzo1fzo0n0  10597  elfzo0z  10598  fzofzim  10602  elfzodifsumelfzo  10621  swrdswrd  11479  swrdccatin1  11499  p1modz1  12563  dfgcd2  12793  algcvga  12831  pcprendvds  13071  usgruspgrben  16439  trlf1  16641