![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > albidv | Unicode version |
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
albidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1416 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | albidv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | albidh 1366 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-17 1416 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11v 1705 2albidv 1744 sbal1yz 1874 eujust 1899 euf 1902 mo23 1938 axext3 2020 bm1.1 2022 eqeq1 2043 nfceqdf 2174 ralbidv2 2322 alexeq 2664 pm13.183 2675 eqeu 2705 mo2icl 2714 euind 2722 reuind 2738 cdeqal 2747 sbcal 2804 sbcalg 2805 sbcabel 2833 csbiebg 2883 ssconb 3070 reldisj 3265 sbcssg 3324 elint 3612 axsep2 3867 zfauscl 3868 bm1.3ii 3869 euotd 3982 eusv1 4150 regexmid 4219 tfisi 4253 nnregexmid 4285 iota5 4830 sbcfung 4868 funimass4 5167 dffo3 5257 eufnfv 5332 dff13 5350 ssfiexmid 6254 fz1sbc 8728 frecuzrdgfn 8879 bdsep2 9341 bdsepnfALT 9344 bdzfauscl 9345 bdbm1.3ii 9346 bj-2inf 9397 bj-nn0sucALT 9438 strcoll2 9443 strcollnfALT 9446 |
Copyright terms: Public domain | W3C validator |