![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimi | GIF version |
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralimi.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
ralimi | ⊢ (∀x ∈ A φ → ∀x ∈ A ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi.1 | . . 3 ⊢ (φ → ψ) | |
2 | 1 | a1i 9 | . 2 ⊢ (x ∈ A → (φ → ψ)) |
3 | 2 | ralimia 2376 | 1 ⊢ (∀x ∈ A φ → ∀x ∈ A ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1390 ∀wral 2300 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 |
This theorem depends on definitions: df-bi 110 df-ral 2305 |
This theorem is referenced by: ral2imi 2379 r19.26 2435 r19.29 2444 rr19.3v 2676 rr19.28v 2677 reu3 2725 uniiunlem 3022 reupick2 3217 uniss2 3602 ss2iun 3663 iineq2 3665 iunss2 3693 disjss2 3739 disjeq2 3740 repizf 3864 reusv3i 4157 tfis 4249 ssrel2 4373 issref 4650 dmmptg 4761 funco 4883 fununi 4910 fun11uni 4912 funimaexglem 4925 fnmpt 4968 fun11iun 5090 mpteqb 5204 chfnrn 5221 dffo5 5259 ffvresb 5271 fmptcof 5274 dfmptg 5285 mpt22eqb 5552 ralrnmpt2 5557 rexrnmpt2 5558 fnmpt2 5770 mpt2exxg 5775 smores 5848 riinerm 6115 cauappcvgprlemdisj 6623 bj-indint 9390 bj-indind 9391 bj-bdfindis 9407 setindis 9427 bdsetindis 9429 |
Copyright terms: Public domain | W3C validator |