![]() |
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 1123 | . 2 ⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) |
3 | 2 | anabsi5 668 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: 3anidm13 1421 syl2an3an 1423 dedth3v 4590 fovcl 7532 nncan 11485 divid 11897 sqdivid 14083 subsq 14170 o1lo1 15477 retancl 16081 tanneg 16087 gcd0id 16456 coprm 16644 ablonncan 29787 kbpj 31187 xdivid 32072 xrsmulgzz 32157 f1resrcmplf1dlem 34027 expgrowthi 43025 dvconstbi 43026 3ornot23 43203 3anidm12p2 43501 sinhpcosh 47687 reseccl 47700 recsccl 47701 recotcl 47702 onetansqsecsq 47708 |
Copyright terms: Public domain | W3C validator |