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 1419 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | albidh 1369 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 wal 1241 |
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 1336 ax-gen 1338 ax-17 1419 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ax11v 1708 2albidv 1747 sbal1yz 1877 eujust 1902 euf 1905 mo23 1941 axext3 2023 bm1.1 2025 eqeq1 2046 nfceqdf 2177 ralbidv2 2328 alexeq 2670 pm13.183 2681 eqeu 2711 mo2icl 2720 euind 2728 reuind 2744 cdeqal 2753 sbcal 2810 sbcalg 2811 sbcabel 2839 csbiebg 2889 ssconb 3076 reldisj 3271 sbcssg 3330 elint 3621 axsep2 3876 zfauscl 3877 bm1.3ii 3878 euotd 3991 freq1 4081 freq2 4083 eusv1 4184 ontr2exmid 4250 regexmid 4260 tfisi 4310 nnregexmid 4342 iota5 4887 sbcfung 4925 funimass4 5224 dffo3 5314 eufnfv 5389 dff13 5407 ssfiexmid 6336 diffitest 6344 findcard 6345 findcard2 6346 findcard2s 6347 fz1sbc 8958 frecuzrdgfn 9198 bdsep2 10006 bdsepnfALT 10009 bdzfauscl 10010 bdbm1.3ii 10011 bj-2inf 10062 bj-nn0sucALT 10103 strcoll2 10108 strcollnfALT 10111 |
Copyright terms: Public domain | W3C validator |