Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.26-2 | Structured version Visualization version Unicode version |
Description: Restricted quantifier version of 19.26-2 1799. Version of r19.26 3064 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
r19.26-2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.26 3064 | . . 3 | |
2 | 1 | ralbii 2980 | . 2 |
3 | r19.26 3064 | . 2 | |
4 | 2, 3 | bitri 264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 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 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ral 2917 |
This theorem is referenced by: fununi 5964 tz7.48lem 7536 isffth2 16576 ispos2 16948 issgrpv 17286 issgrpn0 17287 isnsg2 17624 efgred 18161 dfrhm2 18717 cpmatacl 20521 cpmatmcllem 20523 caucfil 23081 aalioulem6 24092 ajmoi 27714 adjmo 28691 iccllysconn 31232 dfso3 31601 ispridl2 33837 ishlat2 34640 fiinfi 37878 ntrk1k3eqk13 38348 isrnghm 41892 |
Copyright terms: Public domain | W3C validator |