![]() |
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 1465 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.42h 1623 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1427 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exdistr 1836 19.42vv 1837 19.42vvv 1838 4exdistr 1842 cbvex2 1846 2sb5 1908 2sb5rf 1914 rexcom4a 2644 ceqsex2 2660 reuind 2821 2rmorex 2822 sbccomlem 2914 bm1.3ii 3966 opm 4070 eqvinop 4079 uniuni 4286 elco 4615 dmopabss 4661 dmopab3 4662 mptpreima 4937 brprcneu 5311 relelfvdm 5349 fndmin 5420 fliftf 5592 dfoprab2 5710 dmoprab 5743 dmoprabss 5744 fnoprabg 5760 opabex3d 5906 opabex3 5907 eroveu 6397 dmaddpq 6999 dmmulpq 7000 prarloc 7123 ltexprlemopl 7221 ltexprlemlol 7222 ltexprlemopu 7223 ltexprlemupu 7224 shftdm 10317 ntreq0 11893 bdbm1.3ii 12055 |
Copyright terms: Public domain | W3C validator |