Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anassrs | GIF version |
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
anassrs.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
anassrs | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anassrs.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
2 | 1 | exp32 362 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp31 254 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: anass 398 mpanr1 433 anass1rs 560 anabss5 567 anabss7 572 2ralbida 2454 2rexbidva 2456 ralimdvva 2499 pofun 4229 issod 4236 imainss 4949 fvelimab 5470 eqfnfv2 5512 funconstss 5531 fnex 5635 rexima 5649 ralima 5650 f1elima 5667 fliftfun 5690 isores2 5707 isosolem 5718 f1oiso 5720 ovmpodxf 5889 grpridd 5960 tfrlemibxssdm 6217 oav2 6352 omv2 6354 nnaass 6374 eroveu 6513 prarloclem4 7299 genpml 7318 genpmu 7319 genpassl 7325 genpassu 7326 prmuloc2 7368 addcomprg 7379 mulcomprg 7381 ltaddpr 7398 ltexprlemloc 7408 addcanprlemu 7416 recexgt0sr 7574 reapmul1 8350 apreim 8358 recexaplem2 8406 creur 8710 uz11 9341 xaddass 9645 xleadd1a 9649 xlt2add 9656 fzrevral 9878 seq3caopr2 10248 expnlbnd2 10410 shftlem 10581 resqrexlemgt0 10785 cau3lem 10879 clim2 11045 clim2c 11046 clim0c 11048 2clim 11063 climabs0 11069 climcn1 11070 climcn2 11071 climsqz 11097 climsqz2 11098 summodclem2 11144 fsum2dlemstep 11196 fsumiun 11239 mertenslem2 11298 mertensabs 11299 prodfrecap 11308 gcdmultiplez 11698 dvdssq 11708 lcmgcdlem 11747 lcmdvds 11749 coprmdvds2 11763 neipsm 12312 lmbrf 12373 lmss 12404 txbas 12416 txbasval 12425 tx1cn 12427 txlm 12437 isxmet2d 12506 elmopn2 12607 mopni3 12642 blsscls2 12651 metequiv2 12654 metss2lem 12655 metrest 12664 metcnp 12670 metcnp2 12671 metcnpi3 12675 elcncf2 12719 mulc1cncf 12734 cncfco 12736 cncfmet 12737 |
Copyright terms: Public domain | W3C validator |