![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > albidv | GIF 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 1507 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1457 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1330 |
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 ax-17 1507 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1800 2albidv 1840 sbal1yz 1977 eujust 2002 euf 2005 mo23 2041 axext3 2123 bm1.1 2125 eqeq1 2147 nfceqdf 2281 ralbidv2 2440 alexeq 2815 pm13.183 2826 eqeu 2858 mo2icl 2867 euind 2875 reuind 2893 cdeqal 2902 sbcal 2964 sbcalg 2965 sbcabel 2994 csbiebg 3047 ssconb 3214 reldisj 3419 sbcssg 3477 elint 3785 axsep2 4055 zfauscl 4056 bm1.3ii 4057 exmidel 4136 euotd 4184 freq1 4274 freq2 4276 eusv1 4381 ontr2exmid 4448 regexmid 4458 tfisi 4509 nnregexmid 4542 iota5 5116 sbcfung 5155 funimass4 5480 dffo3 5575 eufnfv 5656 dff13 5677 tfr1onlemsucfn 6245 tfr1onlemsucaccv 6246 tfr1onlembxssdm 6248 tfr1onlembfn 6249 tfrcllemsucfn 6258 tfrcllemsucaccv 6259 tfrcllembxssdm 6261 tfrcllembfn 6262 tfrcl 6269 frecabcl 6304 ssfiexmid 6778 domfiexmid 6780 diffitest 6789 findcard 6790 findcard2 6791 findcard2s 6792 fiintim 6825 fisseneq 6828 isomni 7016 isomnimap 7017 ismkv 7035 ismkvmap 7036 iswomni 7047 iswomnimap 7048 omniwomnimkv 7049 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 fz1sbc 9907 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 zfz1iso 10616 istopg 12205 bdsep2 13255 bdsepnfALT 13258 bdzfauscl 13259 bdbm1.3ii 13260 bj-2inf 13307 bj-nn0sucALT 13347 sscoll2 13357 |
Copyright terms: Public domain | W3C validator |