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  954  pm5.63dc  955  simplbi2com  1490  reuss2  3505  elni2  7646  elpq  10003  elfz0ubfz0  10485  elfzmlbp  10492  fzo1fzo0n0  10548  elfzo0z  10549  fzofzim  10553  elfzodifsumelfzo  10572  swrdswrd  11426  swrdccatin1  11446  p1modz1  12510  dfgcd2  12740  algcvga  12778  pcprendvds  13018  usgruspgrben  16312  trlf1  16514