|   | 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 3082 | . 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓) | 
| 3 | 2 | ralimi 3082 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ral 3061 | 
| This theorem is referenced by: 3ralimi 3123 reusv3i 5403 ssrel2 5794 fununi 6640 fnmpo 8095 xpwdomg 9626 catcocl 17729 catpropd 17753 dfgrp3e 19059 rmodislmodlem 20928 rmodislmod 20929 tmdcn2 24098 xmeteq0 24349 xmettri2 24351 mulsuniflem 28176 midf 28785 frgrconngr 30314 ajmoi 30878 adjmo 31852 cnlnssadj 32100 prmidl2 33470 rngodi 37912 rngodir 37913 rngoass 37914 rngohomadd 37977 rngohommul 37978 ispridl2 38046 mpobi123f 38170 ntrk2imkb 44055 gneispaceel 44161 gneispacess 44163 prclaxpr 45007 stoweidlem60 46080 fullthinc 49124 thincciso 49127 | 
| Copyright terms: Public domain | W3C validator |