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 1513 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1467 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1340 |
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 1434 ax-gen 1436 ax-17 1513 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1814 2albidv 1854 sbal1yz 1988 eujust 2015 euf 2018 mo23 2054 axext3 2147 bm1.1 2149 eqeq1 2171 cbvabw 2287 nfceqdf 2305 ralbidv2 2466 alexeq 2850 pm13.183 2862 eqeu 2894 mo2icl 2903 euind 2911 reuind 2929 cdeqal 2938 sbcal 3000 sbcalg 3001 sbcabel 3030 csbcow 3054 csbiebg 3085 ssconb 3253 reldisj 3458 sbcssg 3516 elint 3827 axsep2 4098 zfauscl 4099 bm1.3ii 4100 exmidel 4181 euotd 4229 freq1 4319 freq2 4321 eusv1 4427 ontr2exmid 4499 regexmid 4509 tfisi 4561 nnregexmid 4595 iota5 5170 sbcfung 5209 funimass4 5534 dffo3 5629 eufnfv 5712 dff13 5733 tfr1onlemsucfn 6302 tfr1onlemsucaccv 6303 tfr1onlembxssdm 6305 tfr1onlembfn 6306 tfrcllemsucfn 6315 tfrcllemsucaccv 6316 tfrcllembxssdm 6318 tfrcllembfn 6319 tfrcl 6326 frecabcl 6361 ssfiexmid 6836 domfiexmid 6838 diffitest 6847 findcard 6848 findcard2 6849 findcard2s 6850 fiintim 6888 fisseneq 6891 isomni 7094 isomnimap 7095 ismkv 7111 ismkvmap 7112 iswomni 7123 iswomnimap 7124 omniwomnimkv 7125 exmidfodomrlemr 7152 exmidfodomrlemrALT 7153 fz1sbc 10025 frecuzrdgtcl 10341 frecuzrdgfunlem 10348 zfz1iso 10748 istopg 12595 bdsep2 13661 bdsepnfALT 13664 bdzfauscl 13665 bdbm1.3ii 13666 bj-2inf 13713 bj-nn0sucALT 13753 sscoll2 13763 |
Copyright terms: Public domain | W3C validator |