![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralimi | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
Ref | Expression |
---|---|
ralimi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2ralimi | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ralimi 3125 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralimi 3125 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 |
This theorem depends on definitions: df-bi 208 df-ral 3108 |
This theorem is referenced by: reusv3i 5189 ssrel2 5537 fununi 6291 fnmpo 7614 xpwdomg 8885 catcocl 16773 catpropd 16796 dfgrp3e 17944 rmodislmodlem 19379 rmodislmod 19380 tmdcn2 22369 xmeteq0 22619 xmettri2 22621 midf 26232 frgrconngr 27753 ajmoi 28314 adjmo 29288 cnlnssadj 29536 rngodi 34660 rngodir 34661 rngoass 34662 rngohomadd 34725 rngohommul 34726 ispridl2 34794 mpobi123f 34920 ntrk2imkb 39823 gneispaceel 39929 gneispacess 39931 stoweidlem60 41841 |
Copyright terms: Public domain | W3C validator |