![]() |
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 2876 rr19.28v 2877 reu3 2927 uniiunlem 3244 reupick2 3421 uniss2 3838 ss2iun 3899 iineq2 3901 iunss2 3929 disjss2 3980 disjeq2 3981 disjnim 3991 repizf 4116 abnexg 4442 reusv3i 4455 tfis 4578 ssrel2 4712 issref 5006 dmmptg 5121 funco 5251 fununi 5279 fun11uni 5281 funimaexglem 5294 fnmpt 5337 fun11iun 5477 mpteqb 5601 chfnrn 5622 dffo5 5660 ffvresb 5674 fmptcof 5678 dfmptg 5690 mpo2eqb 5977 ralrnmpo 5982 rexrnmpo 5983 fnmpo 6196 mpoexxg 6204 smores 6286 riinerm 6601 ixpm 6723 difinfinf 7093 nninfwlpoimlemginf 7167 exmidontriimlem1 7213 onntri13 7230 onntri24 7234 cc4f 7246 cc4n 7248 cauappcvgprlemdisj 7628 caucvgsrlemasr 7767 caucvgsr 7779 suplocsr 7786 rexuz3 10970 recvguniq 10975 cau3lem 11094 caubnd2 11097 rexanre 11200 climi2 11267 climi0 11268 climcaucn 11330 ndvdssub 11905 gcdsupex 11928 gcdsupcl 11929 bezoutlemmo 11977 mgmidmo 12670 eltg2b 13187 neipsm 13287 lmcvg 13350 txlm 13412 metrest 13639 mulcncflem 13723 bj-charfunbi 14185 bj-indint 14305 bj-indind 14306 bj-bdfindis 14321 setindis 14341 bdsetindis 14343 |
Copyright terms: Public domain | W3C validator |