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 363 | . 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 399 mpanr1 434 anass1rs 561 anabss5 568 anabss7 573 2ralbida 2485 2rexbidva 2487 ralimdvva 2533 pofun 4284 issod 4291 imainss 5013 fvelimab 5536 eqfnfv2 5578 funconstss 5597 fnex 5701 rexima 5717 ralima 5718 f1elima 5735 fliftfun 5758 isores2 5775 isosolem 5786 f1oiso 5788 ovmpodxf 5958 grpridd 6029 tfrlemibxssdm 6286 oav2 6422 omv2 6424 nnaass 6444 eroveu 6583 prarloclem4 7430 genpml 7449 genpmu 7450 genpassl 7456 genpassu 7457 prmuloc2 7499 addcomprg 7510 mulcomprg 7512 ltaddpr 7529 ltexprlemloc 7539 addcanprlemu 7547 recexgt0sr 7705 reapmul1 8484 apreim 8492 recexaplem2 8540 creur 8845 uz11 9479 xaddass 9796 xleadd1a 9800 xlt2add 9807 fzrevral 10030 seq3caopr2 10407 expnlbnd2 10569 shftlem 10744 resqrexlemgt0 10948 cau3lem 11042 clim2 11210 clim2c 11211 clim0c 11213 2clim 11228 climabs0 11234 climcn1 11235 climcn2 11236 climsqz 11262 climsqz2 11263 summodclem2 11309 fsum2dlemstep 11361 fsumiun 11404 mertenslem2 11463 mertensabs 11464 prodfrecap 11473 fprodeq0 11544 fprod2dlemstep 11549 gcdmultiplez 11939 dvdssq 11949 lcmgcdlem 11988 lcmdvds 11990 coprmdvds2 12004 pclemub 12196 pcge0 12221 pcgcd1 12236 neipsm 12695 lmbrf 12756 lmss 12787 txbas 12799 txbasval 12808 tx1cn 12810 txlm 12820 isxmet2d 12889 elmopn2 12990 mopni3 13025 blsscls2 13034 metequiv2 13037 metss2lem 13038 metrest 13047 metcnp 13053 metcnp2 13054 metcnpi3 13058 elcncf2 13102 mulc1cncf 13117 cncfco 13119 cncfmet 13120 |
Copyright terms: Public domain | W3C validator |