New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3impb | Unicode version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impb.1 |
Ref | Expression |
---|---|
3impb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impb.1 | . . 3 | |
2 | 1 | exp32 588 | . 2 |
3 | 2 | 3imp 1145 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
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 df-3an 936 |
This theorem is referenced by: 3adant1l 1174 3adant1r 1175 3impdi 1237 vtocl3gf 2917 rspc2ev 2963 reuss 3536 pw1equn 4331 pw1eqadj 4332 preaddccan2 4455 resdif 5306 fnopovb 5557 fovrn 5604 fnovrn 5607 mucass 6135 addccan2nc 6265 nchoicelem3 6291 |
Copyright terms: Public domain | W3C validator |