![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.42v | Unicode version |
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.42v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1419 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 19.42h 1577 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: exdistr 1787 19.42vv 1788 19.42vvv 1789 4exdistr 1793 cbvex2 1797 2sb5 1859 2sb5rf 1865 rexcom4a 2578 ceqsex2 2594 reuind 2744 2rmorex 2745 sbccomlem 2832 bm1.3ii 3878 opm 3971 eqvinop 3980 uniuni 4183 dmopabss 4547 dmopab3 4548 mptpreima 4814 brprcneu 5171 relelfvdm 5205 fndmin 5274 fliftf 5439 dfoprab2 5552 dmoprab 5585 dmoprabss 5586 fnoprabg 5602 opabex3d 5748 opabex3 5749 eroveu 6197 dmaddpq 6477 dmmulpq 6478 prarloc 6601 ltexprlemopl 6699 ltexprlemlol 6700 ltexprlemopu 6701 ltexprlemupu 6702 shftdm 9423 bdbm1.3ii 10011 |
Copyright terms: Public domain | W3C validator |