![]() |
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 669 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: 3anidm13 1419 syl2an3an 1421 dedth3v 4594 fovcl 7561 nncan 11536 divid 11951 dividOLD 11952 sqdivid 14159 subsq 14246 o1lo1 15570 retancl 16175 tanneg 16181 gcd0id 16553 coprm 16745 ablonncan 30585 kbpj 31985 xdivid 32895 xrsmulgzz 32994 f1resrcmplf1dlem 35079 expgrowthi 44329 dvconstbi 44330 3ornot23 44507 3anidm12p2 44805 sinhpcosh 48971 reseccl 48984 recsccl 48985 recotcl 48986 onetansqsecsq 48992 |
Copyright terms: Public domain | W3C validator |