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 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | ralimia 2382 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ∀wral 2306 |
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 1336 ax-gen 1338 |
This theorem depends on definitions: df-bi 110 df-ral 2311 |
This theorem is referenced by: ral2imi 2385 r19.26 2441 r19.29 2450 rr19.3v 2682 rr19.28v 2683 reu3 2731 uniiunlem 3028 reupick2 3223 uniss2 3611 ss2iun 3672 iineq2 3674 iunss2 3702 disjss2 3748 disjeq2 3749 repizf 3873 reusv3i 4191 tfis 4306 ssrel2 4430 issref 4707 dmmptg 4818 funco 4940 fununi 4967 fun11uni 4969 funimaexglem 4982 fnmpt 5025 fun11iun 5147 mpteqb 5261 chfnrn 5278 dffo5 5316 ffvresb 5328 fmptcof 5331 dfmptg 5342 mpt22eqb 5610 ralrnmpt2 5615 rexrnmpt2 5616 fnmpt2 5828 mpt2exxg 5833 smores 5907 riinerm 6179 cauappcvgprlemdisj 6749 caucvgsrlemasr 6874 caucvgsr 6886 rexuz3 9588 recvguniq 9593 cau3lem 9710 caubnd2 9713 climi2 9809 climi0 9810 climcaucn 9870 bj-indint 10055 bj-indind 10056 bj-bdfindis 10072 setindis 10092 bdsetindis 10094 |
Copyright terms: Public domain | W3C validator |