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 2952 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralimi 2952 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: reusv3i 4875 ssrel2 5210 fununi 5964 fnmpt2 7238 xpwdomg 8490 catcocl 16346 catpropd 16369 dfgrp3e 17515 rmodislmodlem 18930 rmodislmod 18931 tmdcn2 21893 xmeteq0 22143 xmettri2 22145 midf 25668 frgrconngr 27158 ajmoi 27714 adjmo 28691 cnlnssadj 28939 rngodi 33703 rngodir 33704 rngoass 33705 rngohomadd 33768 rngohommul 33769 ispridl2 33837 mpt2bi123f 33971 ntrk2imkb 38335 gneispaceel 38441 gneispacess 38443 stoweidlem60 40277 |
Copyright terms: Public domain | W3C validator |