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 3157 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralimi 3157 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: reusv3i 5295 ssrel2 5652 fununi 6422 fnmpo 7756 xpwdomg 9037 catcocl 16944 catpropd 16967 dfgrp3e 18137 rmodislmodlem 19630 rmodislmod 19631 tmdcn2 22625 xmeteq0 22875 xmettri2 22877 midf 26489 frgrconngr 28000 ajmoi 28562 adjmo 29536 cnlnssadj 29784 prmidl2 30877 rngodi 35063 rngodir 35064 rngoass 35065 rngohomadd 35128 rngohommul 35129 ispridl2 35197 mpobi123f 35321 ntrk2imkb 40265 gneispaceel 40371 gneispacess 40373 stoweidlem60 42222 |
Copyright terms: Public domain | W3C validator |