![]() |
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 1526 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1480 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wal 1351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-17 1526 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v 1827 2albidv 1867 sbal1yz 2001 eujust 2028 euf 2031 mo23 2067 axext3 2160 bm1.1 2162 eqeq1 2184 cbvabw 2300 nfceqdf 2318 ralbidv2 2479 alexeq 2865 pm13.183 2877 eqeu 2909 mo2icl 2918 euind 2926 reuind 2944 cdeqal 2953 sbcal 3016 sbcalg 3017 sbcabel 3046 csbcow 3070 csbiebg 3101 ssconb 3270 reldisj 3476 sbcssg 3534 elint 3852 axsep2 4124 zfauscl 4125 bm1.3ii 4126 exmidel 4207 euotd 4256 freq1 4346 freq2 4348 eusv1 4454 ontr2exmid 4526 regexmid 4536 tfisi 4588 nnregexmid 4622 iota5 5200 sbcfung 5242 funimass4 5569 dffo3 5666 eufnfv 5750 dff13 5772 tfr1onlemsucfn 6344 tfr1onlemsucaccv 6345 tfr1onlembxssdm 6347 tfr1onlembfn 6348 tfrcllemsucfn 6357 tfrcllemsucaccv 6358 tfrcllembxssdm 6360 tfrcllembfn 6361 tfrcl 6368 frecabcl 6403 ssfiexmid 6879 domfiexmid 6881 diffitest 6890 findcard 6891 findcard2 6892 findcard2s 6893 fiintim 6931 fisseneq 6934 isomni 7137 isomnimap 7138 ismkv 7154 ismkvmap 7155 iswomni 7166 iswomnimap 7167 omniwomnimkv 7168 exmidfodomrlemr 7204 exmidfodomrlemrALT 7205 fz1sbc 10099 frecuzrdgtcl 10415 frecuzrdgfunlem 10422 zfz1iso 10824 istopg 13639 bdsep2 14778 bdsepnfALT 14781 bdzfauscl 14782 bdbm1.3ii 14783 bj-2inf 14830 bj-nn0sucALT 14870 sscoll2 14880 |
Copyright terms: Public domain | W3C validator |