![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbii | Structured version Visualization version Unicode version |
Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
Ref | Expression |
---|---|
ralbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2ralbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralbii 2831 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralbii 2831 |
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 1680 ax-4 1693 |
This theorem depends on definitions: df-bi 190 df-ral 2754 |
This theorem is referenced by: cnvso 5398 fununi 5675 dff14a 6200 isocnv2 6252 sorpss 6608 tpossym 7036 dford2 8156 isffth2 15876 ispos2 16248 issubm 16649 cntzrec 17042 oppgsubm 17068 opprirred 17985 opprsubrg 18084 gsummatr01lem3 19737 gsummatr01 19739 isbasis2g 20018 ist0-3 20416 isfbas2 20905 dfadj2 27594 adjval2 27600 cnlnadjeui 27786 adjbdln 27792 rmo4f 28189 isarchi 28550 iccllyscon 30023 dfso3 30402 elpotr 30477 dfon2 30488 f1opr 32097 isltrn2N 33731 fphpd 35705 isdomn3 36127 fiinfi 36223 ordelordALT 36943 2reu4a 38745 issubmgm 40158 |
Copyright terms: Public domain | W3C validator |