| 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 3078 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: ralimiaa 3082 ralimi 3083 rr19.3v 3667 rr19.28v 3668 exfo 7125 ffvresb 7145 f1mpt 7281 weniso 7374 xpord2indlem 8172 ixpf 8960 ixpiunwdom 9630 tz9.12lem3 9829 dfac2a 10170 kmlem12 10202 axdc2lem 10488 ac6c4 10521 brdom6disj 10572 konigthlem 10608 arch 12523 cshw1 14860 serf0 15717 symgextfo 19440 baspartn 22961 ptcnplem 23629 spanuni 31563 lnopunilem1 32029 phpreu 37611 finixpnum 37612 poimirlem26 37653 indexa 37740 heiborlem5 37822 rngmgmbs4 37938 mzpincl 42745 dfac11 43074 mnurndlem1 44300 natlocalincr 46891 stgoldbwt 47763 2zrngnmlid2 48173 |
| Copyright terms: Public domain | W3C validator |