Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > albidv | Unicode version |
Description: Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 |
Ref | Expression |
---|---|
albidv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1506 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | albidh 1460 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1333 |
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 1427 ax-gen 1429 ax-17 1506 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1807 2albidv 1847 sbal1yz 1981 eujust 2008 euf 2011 mo23 2047 axext3 2140 bm1.1 2142 eqeq1 2164 cbvabw 2280 nfceqdf 2298 ralbidv2 2459 alexeq 2838 pm13.183 2850 eqeu 2882 mo2icl 2891 euind 2899 reuind 2917 cdeqal 2926 sbcal 2988 sbcalg 2989 sbcabel 3018 csbcow 3042 csbiebg 3073 ssconb 3240 reldisj 3445 sbcssg 3503 elint 3813 axsep2 4083 zfauscl 4084 bm1.3ii 4085 exmidel 4166 euotd 4214 freq1 4304 freq2 4306 eusv1 4412 ontr2exmid 4484 regexmid 4494 tfisi 4546 nnregexmid 4580 iota5 5155 sbcfung 5194 funimass4 5519 dffo3 5614 eufnfv 5697 dff13 5718 tfr1onlemsucfn 6287 tfr1onlemsucaccv 6288 tfr1onlembxssdm 6290 tfr1onlembfn 6291 tfrcllemsucfn 6300 tfrcllemsucaccv 6301 tfrcllembxssdm 6303 tfrcllembfn 6304 tfrcl 6311 frecabcl 6346 ssfiexmid 6821 domfiexmid 6823 diffitest 6832 findcard 6833 findcard2 6834 findcard2s 6835 fiintim 6873 fisseneq 6876 isomni 7079 isomnimap 7080 ismkv 7096 ismkvmap 7097 iswomni 7108 iswomnimap 7109 omniwomnimkv 7110 exmidfodomrlemr 7137 exmidfodomrlemrALT 7138 fz1sbc 9998 frecuzrdgtcl 10311 frecuzrdgfunlem 10318 zfz1iso 10712 istopg 12397 bdsep2 13461 bdsepnfALT 13464 bdzfauscl 13465 bdbm1.3ii 13466 bj-2inf 13513 bj-nn0sucALT 13553 sscoll2 13563 |
Copyright terms: Public domain | W3C validator |