![]() |
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 2538 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 |
This theorem depends on definitions: df-bi 117 df-ral 2460 |
This theorem is referenced by: 2ralimi 2541 ral2imi 2542 r19.26 2603 r19.29 2614 rr19.3v 2878 rr19.28v 2879 reu3 2929 uniiunlem 3246 reupick2 3423 uniss2 3842 ss2iun 3903 iineq2 3905 iunss2 3933 disjss2 3985 disjeq2 3986 disjnim 3996 repizf 4121 abnexg 4448 reusv3i 4461 tfis 4584 ssrel2 4718 issref 5013 dmmptg 5128 funco 5258 fununi 5286 fun11uni 5288 funimaexglem 5301 fnmpt 5344 fun11iun 5484 mpteqb 5608 chfnrn 5629 dffo5 5667 ffvresb 5681 fmptcof 5685 dfmptg 5697 mpo2eqb 5986 ralrnmpo 5991 rexrnmpo 5992 fnmpo 6205 mpoexxg 6213 smores 6295 riinerm 6610 ixpm 6732 difinfinf 7102 nninfwlpoimlemginf 7176 exmidontriimlem1 7222 onntri13 7239 onntri24 7243 cc4f 7270 cc4n 7272 cauappcvgprlemdisj 7652 caucvgsrlemasr 7791 caucvgsr 7803 suplocsr 7810 rexuz3 11001 recvguniq 11006 cau3lem 11125 caubnd2 11128 rexanre 11231 climi2 11298 climi0 11299 climcaucn 11361 ndvdssub 11937 gcdsupex 11960 gcdsupcl 11961 bezoutlemmo 12009 ptex 12718 mgmidmo 12796 issubg2m 13054 eltg2b 13593 neipsm 13693 lmcvg 13756 txlm 13818 metrest 14045 mulcncflem 14129 bj-charfunbi 14602 bj-indint 14722 bj-indind 14723 bj-bdfindis 14738 setindis 14758 bdsetindis 14760 neap0mkv 14856 |
Copyright terms: Public domain | W3C validator |