![]() |
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 1465 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | albidh 1415 | 1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1288 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-17 1465 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v 1756 2albidv 1796 sbal1yz 1926 eujust 1951 euf 1954 mo23 1990 axext3 2072 bm1.1 2074 eqeq1 2095 nfceqdf 2228 ralbidv2 2383 alexeq 2744 pm13.183 2755 eqeu 2786 mo2icl 2795 euind 2803 reuind 2821 cdeqal 2830 sbcal 2891 sbcalg 2892 sbcabel 2921 csbiebg 2971 ssconb 3134 reldisj 3338 sbcssg 3395 elint 3700 axsep2 3964 zfauscl 3965 bm1.3ii 3966 exmidel 4042 euotd 4090 freq1 4180 freq2 4182 eusv1 4287 ontr2exmid 4354 regexmid 4364 tfisi 4415 nnregexmid 4447 iota5 5013 sbcfung 5052 funimass4 5368 dffo3 5460 eufnfv 5539 dff13 5561 tfr1onlemsucfn 6119 tfr1onlemsucaccv 6120 tfr1onlembxssdm 6122 tfr1onlembfn 6123 tfrcllemsucfn 6132 tfrcllemsucaccv 6133 tfrcllembxssdm 6135 tfrcllembfn 6136 tfrcl 6143 frecabcl 6178 ssfiexmid 6646 domfiexmid 6648 diffitest 6657 findcard 6658 findcard2 6659 findcard2s 6660 fiintim 6693 fisseneq 6696 isomni 6846 isomnimap 6847 exmidfodomrlemr 6882 exmidfodomrlemrALT 6883 fz1sbc 9564 frecuzrdgtcl 9873 frecuzrdgfunlem 9880 zfz1iso 10300 istopg 11752 bdsep2 12043 bdsepnfALT 12046 bdzfauscl 12047 bdbm1.3ii 12048 bj-2inf 12099 bj-nn0sucALT 12139 strcoll2 12144 strcollnfALT 12147 |
Copyright terms: Public domain | W3C validator |