![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbidva | Structured version Visualization version Unicode version |
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
2ralbidva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2ralbidva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anassrs 658 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralbidva 2835 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ralbidva 2835 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ral 2753 |
This theorem is referenced by: disjxun 4413 isocnv3 6247 isotr 6251 f1oweALT 6803 fnmpt2ovd 6897 tosso 16330 pospropd 16428 isipodrs 16455 mndpropd 16610 mhmpropd 16636 efgred 17446 cmnpropd 17487 ringpropd 17860 lmodprop2d 18198 lsspropd 18288 islmhm2 18309 lmhmpropd 18344 assapropd 18599 islindf4 19444 scmatmats 19584 cpmatel2 19785 1elcpmat 19787 m2cpminvid2 19827 decpmataa0 19840 pmatcollpw2lem 19849 connsub 20484 hausdiag 20708 ist0-4 20792 ismet2 21396 txmetcnp 21610 txmetcn 21611 metuel2 21628 metucn 21634 isngp3 21660 nlmvscn 21738 ipcn 22265 iscfil2 22284 caucfil 22301 cfilresi 22313 ulmdvlem3 23405 cxpcn3 23736 tgcgr4 24624 perpcom 24806 brbtwn2 24983 colinearalglem2 24985 eengtrkg 25063 isarchi2 28550 elmrsubrn 30206 ghomgsg 30359 isbnd3b 32161 iscvlat2N 32934 ishlat3N 32964 gicabl 36001 isdomn3 36125 mgmpropd 40047 mgmhmpropd 40057 lidlmmgm 40197 lindslinindsimp2 40528 |
Copyright terms: Public domain | W3C validator |