![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anidm12 | Structured version Visualization version GIF version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
Ref | Expression |
---|---|
3anidm12.1 | ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
3anidm12 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anidm12.1 | . . 3 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | 3expib 1156 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) |
3 | 2 | anabsi5 659 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 df-an 387 df-3an 1113 |
This theorem is referenced by: 3anidm13 1547 syl2an3an 1549 dedth3v 4369 nncan 10638 divid 11046 sqdivid 13230 subsq 13273 o1lo1 14652 retancl 15251 tanneg 15257 gcd0id 15620 coprm 15801 ablonncan 27962 kbpj 29366 xdivid 30177 xrsmulgzz 30219 expgrowthi 39367 dvconstbi 39368 3ornot23 39548 3anidm12p2 39856 sinhpcosh 43389 reseccl 43402 recsccl 43403 recotcl 43404 onetansqsecsq 43410 |
Copyright terms: Public domain | W3C validator |