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 1121 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) |
3 | 2 | anabsi5 666 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 |
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 206 df-an 397 df-3an 1088 |
This theorem is referenced by: 3anidm13 1419 syl2an3an 1421 dedth3v 4523 nncan 11259 divid 11671 sqdivid 13851 subsq 13935 o1lo1 15255 retancl 15860 tanneg 15866 gcd0id 16235 coprm 16425 ablonncan 28927 kbpj 30327 xdivid 31211 xrsmulgzz 31296 f1resrcmplf1dlem 33067 expgrowthi 41958 dvconstbi 41959 3ornot23 42136 3anidm12p2 42434 sinhpcosh 46453 reseccl 46466 recsccl 46467 recotcl 46468 onetansqsecsq 46474 |
Copyright terms: Public domain | W3C validator |