![]() |
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 360 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: anass 396 mpanr1 431 anass1rs 543 anabss5 550 anabss7 555 2ralbida 2428 2rexbidva 2430 ralimdvva 2473 pofun 4192 issod 4199 imainss 4910 fvelimab 5429 eqfnfv2 5471 funconstss 5490 fnex 5594 rexima 5608 ralima 5609 f1elima 5626 fliftfun 5649 isores2 5666 isosolem 5677 f1oiso 5679 ovmpodxf 5848 grpridd 5919 tfrlemibxssdm 6176 oav2 6311 omv2 6313 nnaass 6333 eroveu 6472 prarloclem4 7248 genpml 7267 genpmu 7268 genpassl 7274 genpassu 7275 prmuloc2 7317 addcomprg 7328 mulcomprg 7330 ltaddpr 7347 ltexprlemloc 7357 addcanprlemu 7365 recexgt0sr 7510 reapmul1 8269 apreim 8277 recexaplem2 8320 creur 8621 uz11 9244 xaddass 9539 xleadd1a 9543 xlt2add 9550 fzrevral 9772 seq3caopr2 10142 expnlbnd2 10304 shftlem 10475 resqrexlemgt0 10678 cau3lem 10772 clim2 10938 clim2c 10939 clim0c 10941 2clim 10956 climabs0 10962 climcn1 10963 climcn2 10964 climsqz 10990 climsqz2 10991 summodclem2 11037 fsum2dlemstep 11089 fsumiun 11132 mertenslem2 11191 mertensabs 11192 gcdmultiplez 11549 dvdssq 11559 lcmgcdlem 11598 lcmdvds 11600 coprmdvds2 11614 neipsm 12160 lmbrf 12220 lmss 12251 txbas 12263 txbasval 12272 tx1cn 12274 txlm 12284 isxmet2d 12331 elmopn2 12432 mopni3 12467 blsscls2 12476 metequiv2 12479 metss2lem 12480 metrest 12489 metcnp 12495 metcnp2 12496 metcnpi3 12500 elcncf2 12541 mulc1cncf 12556 cncfco 12558 cncfmet 12559 |
Copyright terms: Public domain | W3C validator |