![]() |
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 1471 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.42h 1629 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1433 |
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 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exdistr 1842 19.42vv 1843 19.42vvv 1844 4exdistr 1848 cbvex2 1852 2sb5 1914 2sb5rf 1920 rexcom4a 2657 ceqsex2 2673 reuind 2834 2rmorex 2835 sbccomlem 2927 bm1.3ii 3981 opm 4085 eqvinop 4094 uniuni 4301 elco 4633 dmopabss 4679 dmopab3 4680 mptpreima 4958 brprcneu 5333 relelfvdm 5371 fndmin 5445 fliftf 5616 dfoprab2 5734 dmoprab 5767 dmoprabss 5768 fnoprabg 5784 opabex3d 5930 opabex3 5931 eroveu 6423 dmaddpq 7035 dmmulpq 7036 prarloc 7159 ltexprlemopl 7257 ltexprlemlol 7258 ltexprlemopu 7259 ltexprlemupu 7260 shftdm 10371 ntreq0 11984 bdbm1.3ii 12499 |
Copyright terms: Public domain | W3C validator |