![]() |
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 1153 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) |
3 | 2 | anabsi5 660 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 |
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 386 df-3an 1110 |
This theorem is referenced by: 3anidm13 1544 syl2an3an 1546 dedth3v 4338 nncan 10602 divid 11006 sqdivid 13183 subsq 13226 o1lo1 14609 retancl 15208 tanneg 15214 gcd0id 15575 coprm 15756 ablonncan 27936 kbpj 29340 xdivid 30152 xrsmulgzz 30194 expgrowthi 39314 dvconstbi 39315 3ornot23 39495 3anidm12p2 39803 sinhpcosh 43283 reseccl 43296 recsccl 43297 recotcl 43298 onetansqsecsq 43304 |
Copyright terms: Public domain | W3C validator |