![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simplbi2 | GIF version |
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
Ref | Expression |
---|---|
pm3.26bi2.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
simplbi2 | ⊢ (𝜓 → (𝜒 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.26bi2.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | biimpri 133 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑) |
3 | 2 | ex 115 | 1 ⊢ (𝜓 → (𝜒 → 𝜑)) |
Colors of variables: wff set class |
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 945 pm5.63dc 946 simplbi2com 1444 reuss2 3417 elni2 7315 elpq 9650 elfz0ubfz0 10127 elfzmlbp 10134 fzo1fzo0n0 10185 elfzo0z 10186 fzofzim 10190 elfzodifsumelfzo 10203 p1modz1 11803 dfgcd2 12017 algcvga 12053 pcprendvds 12292 |
Copyright terms: Public domain | W3C validator |