Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.29 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.29 1789. See also r19.29r 3055. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.29 | ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 462 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
2 | 1 | ralimi 2936 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓))) |
3 | rexim 2991 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
5 | 4 | imp 444 | 1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: r19.29r 3055 r19.29d2r 3061 disjiun 4573 triun 4694 ralxfrd 4805 ralxfrdOLD 4806 ralxfrd2 4810 elrnmptg 5296 fmpt 6289 fliftfun 6462 fun11iun 7019 omabs 7614 findcard3 8088 r1sdom 8520 tcrank 8630 infxpenlem 8719 dfac12k 8852 cfslb2n 8973 cfcoflem 8977 iundom2g 9241 supsrlem 9811 axpre-sup 9869 fimaxre3 10849 limsupbnd2 14062 rlimuni 14129 rlimcld2 14157 rlimno1 14232 pgpfac1lem5 18301 ppttop 20621 epttop 20623 tgcnp 20867 lmcnp 20918 bwth 21023 1stcrest 21066 txlm 21261 tx1stc 21263 fbfinnfr 21455 fbunfip 21483 filuni 21499 ufileu 21533 fbflim2 21591 flftg 21610 ufilcmp 21646 cnpfcf 21655 tsmsxp 21768 metss 22123 lmmbr 22864 ivthlem2 23028 ivthlem3 23029 dyadmax 23172 rhmdvdsr 29149 tpr2rico 29286 esumpcvgval 29467 sigaclcuni 29508 voliune 29619 volfiniune 29620 dya2icoseg2 29667 poimirlem29 32608 unirep 32677 heibor1lem 32778 2r19.29 33160 pmapglbx 34073 stoweidlem35 38928 |
Copyright terms: Public domain | W3C validator |