New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpcom | Unicode version |
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.) |
Ref | Expression |
---|---|
mpcom.1 | |
mpcom.2 |
Ref | Expression |
---|---|
mpcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpcom.1 | . 2 | |
2 | mpcom.2 | . . 3 | |
3 | 2 | com12 27 | . 2 |
4 | 1, 3 | mpd 14 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8 |
This theorem is referenced by: syldan 456 ax16i 2046 ceqex 2969 unsneqsn 3887 sfintfin 4532 0cnelphi 4597 vtoclr 4816 opeldm 4910 tz6.12-1 5344 tz6.12c 5347 fununiq 5517 oprabid 5550 eloprabga 5578 ndmovordi 5621 clos1conn 5879 enmap2lem3 6065 enmap2 6068 enmap1lem3 6071 enpw 6087 ce0nnuli 6178 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |