![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imnan | GIF version |
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.) |
Ref | Expression |
---|---|
imnan | ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2im 599 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 122 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | 2 | con2i 590 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
4 | pm3.2 137 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
5 | 4 | con3rr3 596 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓)) |
6 | 3, 5 | impbii 124 | 1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: imnani 658 nan 659 pm3.24 660 imandc 820 ianordc 833 pm5.17dc 844 dn1dc 902 xorbin 1316 xordc1 1325 alinexa 1535 dfrex2dc 2365 ralinexa 2399 rabeq0 3295 disj 3313 minel 3326 disjsn 3478 sotricim 4114 poirr2 4779 funun 5011 imadiflem 5046 imadif 5047 brprcneu 5246 prltlu 6949 caucvgprlemnbj 7129 caucvgprprlemnbj 7155 xrltnsym2 9159 fzp1nel 9411 phiprmpw 10978 |
Copyright terms: Public domain | W3C validator |