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  958  pm5.63dc  959  simplbi2com  1494  reuss2  3513  elni2  7675  elpq  10032  elfz0ubfz0  10515  elfzmlbp  10522  fzo1fzo0n0  10578  elfzo0z  10579  fzofzim  10583  elfzodifsumelfzo  10602  swrdswrd  11460  swrdccatin1  11480  p1modz1  12544  dfgcd2  12774  algcvga  12812  pcprendvds  13052  usgruspgrben  16410  trlf1  16612