![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.42v | Structured version Visualization version GIF version |
Description: Version of 19.42 2261 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
19.42v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v 2029 | . 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
2 | exancom 1938 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
3 | ancom 452 | . 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 292 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 |
This theorem is referenced by: exdistr 2034 19.42vv 2035 19.42vvv 2036 4exdistr 2039 2sb5 2276 eeeanv 2345 rexcom4a 3378 ceqsex2 3396 reuind 3563 2reu5lem3 3567 sbccomlem 3658 bm1.3ii 4918 eqvinop 5082 dmopabss 5474 dmopab3 5475 mptpreima 5772 mptfnf 6155 brprcneu 6325 fndmin 6467 fliftf 6708 dfoprab2 6848 dmoprab 6888 dmoprabss 6889 fnoprabg 6908 uniuni 7118 zfrep6 7281 opabex3d 7292 opabex3 7293 fsplit 7433 eroveu 7995 rankuni 8890 aceq1 9140 dfac3 9144 kmlem14 9187 kmlem15 9188 axdc2lem 9472 1idpr 10053 ltexprlem1 10060 ltexprlem4 10063 xpcogend 13923 shftdm 14019 joindm 17211 meetdm 17225 toprntopon 20950 ntreq0 21102 cnextf 22090 adjeu 29088 rexunirn 29670 fpwrelmapffslem 29847 tgoldbachgt 31081 bnj1019 31188 bnj1209 31205 bnj1033 31375 bnj1189 31415 dmscut 32255 dfiota3 32367 brimg 32381 funpartlem 32386 bj-eeanvw 33041 bj-rexcom4 33198 bj-rexcom4a 33199 bj-snsetex 33282 bj-snglc 33288 bj-bm1.3ii 33355 bj-restuni 33382 itg2addnc 33796 sbccom2lem 34261 eldmres 34379 rnxrn 34498 rp-isfinite6 38390 undmrnresiss 38436 elintima 38471 pm11.58 39116 pm11.71 39123 2sbc5g 39143 iotasbc2 39147 ax6e2nd 39299 ax6e2ndVD 39666 ax6e2ndALT 39688 stoweidlem60 40794 elpglem3 42987 |
Copyright terms: Public domain | W3C validator |