Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anidm23 | Structured version Visualization version GIF version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.) |
Ref | Expression |
---|---|
3anidm23.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
3anidm23 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anidm23.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) | |
2 | 1 | 3expa 1110 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) |
3 | 2 | anabss3 671 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: supsn 8924 infsn 8957 grusn 10214 subeq0 10900 halfaddsub 11858 avglt2 11864 modabs2 13261 efsub 15441 sinmul 15513 divalgmod 15745 modgcd 15868 pythagtriplem4 16144 pythagtriplem16 16155 pltirr 17561 latjidm 17672 latmidm 17684 ipopos 17758 mulgmodid 18204 f1omvdcnv 18501 lsmss1 18720 zntoslem 20631 obsipid 20794 smadiadetlem2 21201 smadiadet 21207 ordtt1 21915 xmet0 22879 nmsq 23725 tcphcphlem3 23763 tcphcph 23767 grpoidinvlem1 28208 grpodivid 28246 nvmid 28363 ipidsq 28414 5oalem1 29358 3oalem2 29367 unopf1o 29620 unopnorm 29621 hmopre 29627 ballotlemfc0 31649 ballotlemfcc 31650 pdivsq 32878 gcdabsorb 32881 cgr3rflx 33412 endofsegid 33443 tailini 33621 nnssi2 33700 nndivlub 33703 brin2 35537 opoccl 36210 opococ 36211 opexmid 36223 opnoncon 36224 cmtidN 36273 ltrniotaidvalN 37599 pell14qrexpclnn0 39341 rmxdbl 39414 rmydbl 39415 rhmsubclem3 44287 rhmsubcALTVlem3 44305 |
Copyright terms: Public domain | W3C validator |