New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pm3.2i | Unicode version |
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
pm3.2i.1 | |
pm3.2i.2 |
Ref | Expression |
---|---|
pm3.2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2i.1 | . 2 | |
2 | pm3.2i.2 | . 2 | |
3 | pm3.2 434 | . 2 | |
4 | 1, 2, 3 | mp2 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 358 |
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 177 df-an 360 |
This theorem is referenced by: pm4.87 567 dfbi 610 mp4an 654 3pm3.2i 1130 pm11.07 2115 unssi 3439 ssini 3479 elvvk 4208 ncfinraise 4482 evenoddnnnul 4515 brsi 4762 nfunv 5139 caovcom 5626 mpt2v 5720 op1st2nd 5791 fnfullfun 5859 bren 6031 endisj 6052 ce0addcnnul 6180 |
Copyright terms: Public domain | W3C validator |