![]() |
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 |
---|---|
2ralimi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2ralimi | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralimi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ralimi 3078 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) |
3 | 2 | ralimi 3078 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3056 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-ral 3057 |
This theorem is referenced by: 3ralimi 3119 reusv3i 5398 ssrel2 5781 fununi 6622 fnmpo 8067 xpwdomg 9602 catcocl 17658 catpropd 17682 dfgrp3e 18989 rmodislmodlem 20805 rmodislmod 20806 rmodislmodOLD 20807 tmdcn2 23986 xmeteq0 24237 xmettri2 24239 mulsuniflem 28042 midf 28573 frgrconngr 30097 ajmoi 30661 adjmo 31635 cnlnssadj 31883 prmidl2 33146 rngodi 37366 rngodir 37367 rngoass 37368 rngohomadd 37431 rngohommul 37432 ispridl2 37500 mpobi123f 37624 ntrk2imkb 43439 gneispaceel 43545 gneispacess 43547 stoweidlem60 45420 fullthinc 48024 thincciso 48027 |
Copyright terms: Public domain | W3C validator |