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  947  pm5.63dc  948  simplbi2com  1455  reuss2  3444  elni2  7384  elpq  9726  elfz0ubfz0  10203  elfzmlbp  10210  fzo1fzo0n0  10262  elfzo0z  10263  fzofzim  10267  elfzodifsumelfzo  10280  p1modz1  11962  dfgcd2  12192  algcvga  12230  pcprendvds  12470