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 3080 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralimi 3080 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-ral 3063 |
This theorem is referenced by: reusv3i 5294 ssrel2 5653 fununi 6452 fnmpo 7836 xpwdomg 9198 catcocl 17185 catpropd 17209 dfgrp3e 18460 rmodislmodlem 19963 rmodislmod 19964 tmdcn2 22983 xmeteq0 23233 xmettri2 23235 midf 26864 frgrconngr 28374 ajmoi 28936 adjmo 29910 cnlnssadj 30158 prmidl2 31327 xpord3ind 33534 rngodi 35797 rngodir 35798 rngoass 35799 rngohomadd 35862 rngohommul 35863 ispridl2 35931 mpobi123f 36055 ntrk2imkb 41322 gneispaceel 41428 gneispacess 41430 stoweidlem60 43274 fullthinc 45998 thincciso 46001 |
Copyright terms: Public domain | W3C validator |