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 2980 | . 2 |
3 | 2 | ralbii 2980 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 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-ral 2917 |
This theorem is referenced by: cnvso 5674 fununi 5964 dff14a 6527 isocnv2 6581 sorpss 6942 tpossym 7384 dford2 8517 isffth2 16576 ispos2 16948 issubm 17347 cntzrec 17766 oppgsubm 17792 opprirred 18702 opprsubrg 18801 gsummatr01lem3 20463 gsummatr01 20465 isbasis2g 20752 ist0-3 21149 isfbas2 21639 isclmp 22897 dfadj2 28744 adjval2 28750 cnlnadjeui 28936 adjbdln 28942 rmo4f 29337 isarchi 29736 iccllysconn 31232 dfso3 31601 elpotr 31686 dfon2 31697 f1opr 33519 3ralbii 34013 idinxpss 34083 inxpssidinxp 34086 idinxpssinxp 34087 isltrn2N 35406 fphpd 37380 isdomn3 37782 fiinfi 37878 ntrk1k3eqk13 38348 ordelordALT 38747 2reu4a 41189 issubmgm 41789 |
Copyright terms: Public domain | W3C validator |