![]() |
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 1416 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 19.42h 1574 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: exdistr 1784 19.42vv 1785 19.42vvv 1786 4exdistr 1790 cbvex2 1794 2sb5 1856 2sb5rf 1862 rexcom4a 2572 ceqsex2 2588 reuind 2738 2rmorex 2739 sbccomlem 2826 bm1.3ii 3869 opm 3962 eqvinop 3971 uniuni 4149 dmopabss 4490 dmopab3 4491 mptpreima 4757 brprcneu 5114 relelfvdm 5148 fndmin 5217 fliftf 5382 dfoprab2 5494 dmoprab 5527 dmoprabss 5528 fnoprabg 5544 opabex3d 5690 opabex3 5691 eroveu 6133 dmaddpq 6363 dmmulpq 6364 prarloc 6486 ltexprlemopl 6575 ltexprlemlol 6576 ltexprlemopu 6577 ltexprlemupu 6578 bdbm1.3ii 9346 |
Copyright terms: Public domain | W3C validator |