![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimia | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
Ref | Expression |
---|---|
ralimia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
ralimia | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
2 | 1 | a2i 14 | . 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralimi2 3079 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ral 3063 |
This theorem is referenced by: ralimiaa 3083 ralimi 3084 rr19.3v 3657 rr19.28v 3658 exfo 7104 ffvresb 7121 f1mpt 7257 weniso 7348 xpord2indlem 8130 ixpf 8911 ixpiunwdom 9582 tz9.12lem3 9781 dfac2a 10121 kmlem12 10153 axdc2lem 10440 ac6c4 10473 brdom6disj 10524 konigthlem 10560 arch 12466 cshw1 14769 serf0 15624 symgextfo 19285 baspartn 22449 ptcnplem 23117 spanuni 30785 lnopunilem1 31251 phpreu 36461 finixpnum 36462 poimirlem26 36503 indexa 36590 heiborlem5 36672 rngmgmbs4 36788 mzpincl 41458 dfac11 41790 mnurndlem1 43026 natlocalincr 45577 stgoldbwt 46431 2zrngnmlid2 46803 |
Copyright terms: Public domain | W3C validator |