![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > andir | Structured version Visualization version Unicode version |
Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Ref | Expression |
---|---|
andir |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | andi 883 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ancom 456 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ancom 456 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | ancom 456 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | orbi12i 528 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | 3bitr4i 285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-or 376 df-an 377 |
This theorem is referenced by: anddi 886 cases 988 cador 1522 rexun 3626 rabun2 3734 reuun2 3738 xpundir 4907 coundi 5355 mptun 5731 tpostpos 7019 wemapsolem 8091 ltxr 11444 hashbclem 12648 hashf1lem2 12652 pythagtriplem2 14816 pythagtrip 14833 vdwapun 14973 legtrid 24685 colinearalg 24989 usgraedg4 25163 vdgrun 25678 vdgrfiun 25679 elimifd 28209 dfon2lem5 30482 nobndup 30638 nofulllem5 30644 seglelin 30932 poimirlem30 32015 poimirlem31 32016 cnambfre 32034 expdioph 35923 rp-isfinite6 36208 vtxduhgrun 39588 usgvincvad 39989 usgvincvadALT 39992 |
Copyright terms: Public domain | W3C validator |