New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pm3.2i | GIF 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 3438 ssini 3478 elvvk 4207 ncfinraise 4481 evenoddnnnul 4514 brsi 4761 nfunv 5138 caovcom 5625 mpt2v 5719 op1st2nd 5790 fnfullfun 5858 bren 6030 endisj 6051 ce0addcnnul 6179 |
Copyright terms: Public domain | W3C validator |