|   | 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 1122 | . 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 1421 syl2an3an 1423 dedth3v 4588 fovcl 7562 nncan 11539 divid 11954 dividOLD 11955 sqdivid 14163 subsq 14250 o1lo1 15574 retancl 16179 tanneg 16185 gcd0id 16557 coprm 16749 ablonncan 30576 kbpj 31976 xdivid 32911 xrsmulgzz 33012 f1resrcmplf1dlem 35101 expgrowthi 44357 dvconstbi 44358 3ornot23 44534 3anidm12p2 44832 sinhpcosh 49314 reseccl 49327 recsccl 49328 recotcl 49329 onetansqsecsq 49335 | 
| Copyright terms: Public domain | W3C validator |