![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2albii | Structured version Visualization version Unicode version |
Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
albii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2albii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albii.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | albii 1702 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | albii 1702 |
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 |
This theorem is referenced by: sbcom2 2285 2sb6rf 2292 mo4f 2356 2mo2 2390 2mos 2392 r3al 2780 ralcomf 2961 nfnid 4643 raliunxp 4993 cnvsym 5233 intasym 5234 intirr 5237 codir 5239 qfto 5240 dffun4 5613 fun11 5670 fununi 5671 mpt22eqb 6432 aceq0 8575 zfac 8916 zfcndac 9070 addsrmo 9523 mulsrmo 9524 cotr2g 13089 isirred2 17978 2spotdisj 25838 rmo4fOLD 28181 bnj580 29773 bnj978 29809 axacprim 30383 dfso2 30443 dfpo2 30444 dfon2lem8 30485 dffun10 30730 wl-sbcom2d 31936 mpt2bi123f 32451 dford4 35929 isdomn3 36126 undmrnresiss 36255 cnvssco 36257 pm14.12 36816 |
Copyright terms: Public domain | W3C validator |