![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2albii | Unicode version |
Description: Inference adding 2 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 1447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | albii 1447 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mor 2042 mo4f 2060 moanim 2074 2eu4 2093 ralcomf 2595 raliunxp 4688 cnvsym 4930 intasym 4931 intirr 4933 codir 4935 qfto 4936 dffun4 5142 dffun4f 5147 funcnveq 5194 fun11 5198 fununi 5199 mpo2eqb 5888 addnq0mo 7279 mulnq0mo 7280 addsrmo 7575 mulsrmo 7576 |
Copyright terms: Public domain | W3C validator |