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 1506 | . 2 | |
2 | 1 | 19.42h 1665 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exdistr 1881 19.42vv 1883 19.42vvv 1884 4exdistr 1888 cbvex2 1894 2sb5 1958 2sb5rf 1964 rexcom4a 2710 ceqsex2 2726 reuind 2889 2rmorex 2890 sbccomlem 2983 bm1.3ii 4049 opm 4156 eqvinop 4165 uniuni 4372 elco 4705 dmopabss 4751 dmopab3 4752 mptpreima 5032 brprcneu 5414 relelfvdm 5453 fndmin 5527 fliftf 5700 dfoprab2 5818 dmoprab 5852 dmoprabss 5853 fnoprabg 5872 opabex3d 6019 opabex3 6020 eroveu 6520 dmaddpq 7187 dmmulpq 7188 prarloc 7311 ltexprlemopl 7409 ltexprlemlol 7410 ltexprlemopu 7411 ltexprlemupu 7412 shftdm 10594 ntreq0 12301 bdbm1.3ii 13089 |
Copyright terms: Public domain | W3C validator |