![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.42v | GIF 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 1537 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.42h 1698 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∃wex 1503 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: exdistr 1921 19.42vv 1923 19.42vvv 1924 4exdistr 1928 cbvex2 1934 2sb5 1995 2sb5rf 2001 rexcom4a 2776 ceqsex2 2792 reuind 2957 2rmorex 2958 sbccomlem 3052 bm1.3ii 4139 opm 4249 eqvinop 4258 uniuni 4466 elco 4808 dmopabss 4854 dmopab3 4855 mptpreima 5137 brprcneu 5523 relelfvdm 5562 fndmin 5639 fliftf 5816 dfoprab2 5938 dmoprab 5972 dmoprabss 5973 fnoprabg 5992 opabex3d 6140 opabex3 6141 eroveu 6644 dmaddpq 7396 dmmulpq 7397 prarloc 7520 ltexprlemopl 7618 ltexprlemlol 7619 ltexprlemopu 7620 ltexprlemupu 7621 shftdm 10849 ntreq0 14029 bdbm1.3ii 15040 |
Copyright terms: Public domain | W3C validator |