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 2525 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 ∀wral 2442 |
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 1434 ax-gen 1436 |
This theorem depends on definitions: df-bi 116 df-ral 2447 |
This theorem is referenced by: 2ralimi 2528 ral2imi 2529 r19.26 2590 r19.29 2601 rr19.3v 2860 rr19.28v 2861 reu3 2911 uniiunlem 3226 reupick2 3403 uniss2 3814 ss2iun 3875 iineq2 3877 iunss2 3905 disjss2 3956 disjeq2 3957 disjnim 3967 repizf 4092 abnexg 4418 reusv3i 4431 tfis 4554 ssrel2 4688 issref 4980 dmmptg 5095 funco 5222 fununi 5250 fun11uni 5252 funimaexglem 5265 fnmpt 5308 fun11iun 5447 mpteqb 5570 chfnrn 5590 dffo5 5628 ffvresb 5642 fmptcof 5646 dfmptg 5658 mpo2eqb 5942 ralrnmpo 5947 rexrnmpo 5948 fnmpo 6162 mpoexxg 6170 smores 6251 riinerm 6565 ixpm 6687 difinfinf 7057 exmidontriimlem1 7168 onntri13 7185 onntri24 7189 cc4f 7201 cc4n 7203 cauappcvgprlemdisj 7583 caucvgsrlemasr 7722 caucvgsr 7734 suplocsr 7741 rexuz3 10918 recvguniq 10923 cau3lem 11042 caubnd2 11045 rexanre 11148 climi2 11215 climi0 11216 climcaucn 11278 ndvdssub 11852 gcdsupex 11875 gcdsupcl 11876 bezoutlemmo 11924 eltg2b 12601 neipsm 12701 lmcvg 12764 txlm 12826 metrest 13053 mulcncflem 13137 bj-charfunbi 13534 bj-indint 13654 bj-indind 13655 bj-bdfindis 13670 setindis 13690 bdsetindis 13692 |
Copyright terms: Public domain | W3C validator |