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 1519 | . 2 | |
2 | albidv.1 | . 2 | |
3 | 1, 2 | albidh 1473 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1346 |
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 1440 ax-gen 1442 ax-17 1519 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1820 2albidv 1860 sbal1yz 1994 eujust 2021 euf 2024 mo23 2060 axext3 2153 bm1.1 2155 eqeq1 2177 cbvabw 2293 nfceqdf 2311 ralbidv2 2472 alexeq 2856 pm13.183 2868 eqeu 2900 mo2icl 2909 euind 2917 reuind 2935 cdeqal 2944 sbcal 3006 sbcalg 3007 sbcabel 3036 csbcow 3060 csbiebg 3091 ssconb 3260 reldisj 3466 sbcssg 3524 elint 3837 axsep2 4108 zfauscl 4109 bm1.3ii 4110 exmidel 4191 euotd 4239 freq1 4329 freq2 4331 eusv1 4437 ontr2exmid 4509 regexmid 4519 tfisi 4571 nnregexmid 4605 iota5 5180 sbcfung 5222 funimass4 5547 dffo3 5643 eufnfv 5726 dff13 5747 tfr1onlemsucfn 6319 tfr1onlemsucaccv 6320 tfr1onlembxssdm 6322 tfr1onlembfn 6323 tfrcllemsucfn 6332 tfrcllemsucaccv 6333 tfrcllembxssdm 6335 tfrcllembfn 6336 tfrcl 6343 frecabcl 6378 ssfiexmid 6854 domfiexmid 6856 diffitest 6865 findcard 6866 findcard2 6867 findcard2s 6868 fiintim 6906 fisseneq 6909 isomni 7112 isomnimap 7113 ismkv 7129 ismkvmap 7130 iswomni 7141 iswomnimap 7142 omniwomnimkv 7143 exmidfodomrlemr 7179 exmidfodomrlemrALT 7180 fz1sbc 10052 frecuzrdgtcl 10368 frecuzrdgfunlem 10375 zfz1iso 10776 istopg 12791 bdsep2 13921 bdsepnfALT 13924 bdzfauscl 13925 bdbm1.3ii 13926 bj-2inf 13973 bj-nn0sucALT 14013 sscoll2 14023 |
Copyright terms: Public domain | W3C validator |