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 2531 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∀wral 2448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 |
This theorem depends on definitions: df-bi 116 df-ral 2453 |
This theorem is referenced by: 2ralimi 2534 ral2imi 2535 r19.26 2596 r19.29 2607 rr19.3v 2869 rr19.28v 2870 reu3 2920 uniiunlem 3236 reupick2 3413 uniss2 3827 ss2iun 3888 iineq2 3890 iunss2 3918 disjss2 3969 disjeq2 3970 disjnim 3980 repizf 4105 abnexg 4431 reusv3i 4444 tfis 4567 ssrel2 4701 issref 4993 dmmptg 5108 funco 5238 fununi 5266 fun11uni 5268 funimaexglem 5281 fnmpt 5324 fun11iun 5463 mpteqb 5586 chfnrn 5607 dffo5 5645 ffvresb 5659 fmptcof 5663 dfmptg 5675 mpo2eqb 5962 ralrnmpo 5967 rexrnmpo 5968 fnmpo 6181 mpoexxg 6189 smores 6271 riinerm 6586 ixpm 6708 difinfinf 7078 nninfwlpoimlemginf 7152 exmidontriimlem1 7198 onntri13 7215 onntri24 7219 cc4f 7231 cc4n 7233 cauappcvgprlemdisj 7613 caucvgsrlemasr 7752 caucvgsr 7764 suplocsr 7771 rexuz3 10954 recvguniq 10959 cau3lem 11078 caubnd2 11081 rexanre 11184 climi2 11251 climi0 11252 climcaucn 11314 ndvdssub 11889 gcdsupex 11912 gcdsupcl 11913 bezoutlemmo 11961 mgmidmo 12626 eltg2b 12848 neipsm 12948 lmcvg 13011 txlm 13073 metrest 13300 mulcncflem 13384 bj-charfunbi 13846 bj-indint 13966 bj-indind 13967 bj-bdfindis 13982 setindis 14002 bdsetindis 14004 |
Copyright terms: Public domain | W3C validator |