![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exp32 | Unicode version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp32.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exp32 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp32.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | expd 258 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: exp44 373 exp45 374 expr 375 anassrs 400 an13s 567 3impb 1199 xordidc 1399 f0rn0 5410 funfvima3 5750 isoini 5818 ovg 6012 fundmen 6805 distrlem1prl 7580 distrlem1pru 7581 caucvgprprlemaddq 7706 recexgt0sr 7771 axpre-suploclemres 7899 cnegexlem2 8132 mulgt1 8819 faclbnd 10720 divgcdcoprm0 12100 cncongr2 12103 oddpwdclemdvds 12169 oddpwdclemndvds 12170 infpnlem1 12356 cnpnei 13689 zabsle1 14370 |
Copyright terms: Public domain | W3C validator |