![]() |
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 1526 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 19.42h 1687 |
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-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: exdistr 1909 19.42vv 1911 19.42vvv 1912 4exdistr 1916 cbvex2 1922 2sb5 1983 2sb5rf 1989 rexcom4a 2761 ceqsex2 2777 reuind 2942 2rmorex 2943 sbccomlem 3037 bm1.3ii 4124 opm 4234 eqvinop 4243 uniuni 4451 elco 4793 dmopabss 4839 dmopab3 4840 mptpreima 5122 brprcneu 5508 relelfvdm 5547 fndmin 5623 fliftf 5799 dfoprab2 5921 dmoprab 5955 dmoprabss 5956 fnoprabg 5975 opabex3d 6121 opabex3 6122 eroveu 6625 dmaddpq 7377 dmmulpq 7378 prarloc 7501 ltexprlemopl 7599 ltexprlemlol 7600 ltexprlemopu 7601 ltexprlemupu 7602 shftdm 10826 ntreq0 13563 bdbm1.3ii 14563 |
Copyright terms: Public domain | W3C validator |