Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbid | Structured version Visualization version Unicode version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
ralbid.1 | |
ralbid.2 |
Ref | Expression |
---|---|
ralbid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbid.1 | . 2 | |
2 | ralbid.2 | . . 3 | |
3 | 2 | adantr 481 | . 2 |
4 | 1, 3 | ralbida 2982 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wnf 1708 wcel 1990 wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-nf 1710 df-ral 2917 |
This theorem is referenced by: raleqbid 3150 sbcralt 3510 sbcrext 3511 sbcrextOLD 3512 riota5f 6636 zfrep6 7134 cnfcom3clem 8602 cplem2 8753 infxpenc2lem2 8843 acnlem 8871 lble 10975 fsuppmapnn0fiubex 12792 chirred 29254 aciunf1lem 29462 nosupbnd1 31860 indexa 33528 riotasvd 34242 cdlemk36 36201 choicefi 39392 axccdom 39416 rexabsle 39646 infxrunb3rnmpt 39655 uzublem 39657 climf 39854 climf2 39898 limsupubuzlem 39944 cncficcgt0 40101 stoweidlem16 40233 stoweidlem18 40235 stoweidlem21 40238 stoweidlem29 40246 stoweidlem31 40248 stoweidlem36 40253 stoweidlem41 40258 stoweidlem44 40261 stoweidlem45 40262 stoweidlem51 40268 stoweidlem55 40272 stoweidlem59 40276 stoweidlem60 40277 issmfgelem 40977 smfpimcclem 41013 sprsymrelf 41745 |
Copyright terms: Public domain | W3C validator |