![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pm3.21 | Unicode version |
Description: Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
pm3.21 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 435 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 29 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem is referenced by: pm3.22 437 iba 490 ancr 533 anc2r 540 pm5.31 572 19.41 1896 19.41OLD 1897 2mo 2336 smoord 6590 fisupg 7318 winalim2 8531 aalioulem5 20210 musum 20933 chrelat2i 23825 relin01 25151 waj-ax 26072 pm11.71 27468 ssfz12 27980 onfrALTlem2 28347 19.41rg 28352 onfrALTlem2VD 28714 2pm13.193VD 28728 a9e2eqVD 28732 bnj1173 29081 hlrelat2 29889 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 df-an 361 |
Copyright terms: Public domain | W3C validator |