![]() |
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 1507 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.42h 1666 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1469 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exdistr 1882 19.42vv 1884 19.42vvv 1885 4exdistr 1889 cbvex2 1895 2sb5 1959 2sb5rf 1965 rexcom4a 2713 ceqsex2 2729 reuind 2893 2rmorex 2894 sbccomlem 2987 bm1.3ii 4057 opm 4164 eqvinop 4173 uniuni 4380 elco 4713 dmopabss 4759 dmopab3 4760 mptpreima 5040 brprcneu 5422 relelfvdm 5461 fndmin 5535 fliftf 5708 dfoprab2 5826 dmoprab 5860 dmoprabss 5861 fnoprabg 5880 opabex3d 6027 opabex3 6028 eroveu 6528 dmaddpq 7211 dmmulpq 7212 prarloc 7335 ltexprlemopl 7433 ltexprlemlol 7434 ltexprlemopu 7435 ltexprlemupu 7436 shftdm 10626 ntreq0 12340 bdbm1.3ii 13260 |
Copyright terms: Public domain | W3C validator |