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 1491 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.42h 1650 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1453 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exdistr 1863 19.42vv 1865 19.42vvv 1866 4exdistr 1870 cbvex2 1874 2sb5 1936 2sb5rf 1942 rexcom4a 2684 ceqsex2 2700 reuind 2862 2rmorex 2863 sbccomlem 2955 bm1.3ii 4019 opm 4126 eqvinop 4135 uniuni 4342 elco 4675 dmopabss 4721 dmopab3 4722 mptpreima 5002 brprcneu 5382 relelfvdm 5421 fndmin 5495 fliftf 5668 dfoprab2 5786 dmoprab 5820 dmoprabss 5821 fnoprabg 5840 opabex3d 5987 opabex3 5988 eroveu 6488 dmaddpq 7155 dmmulpq 7156 prarloc 7279 ltexprlemopl 7377 ltexprlemlol 7378 ltexprlemopu 7379 ltexprlemupu 7380 shftdm 10562 ntreq0 12228 bdbm1.3ii 13016 |
Copyright terms: Public domain | W3C validator |