Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > albii | GIF version |
Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
albii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
albii | ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albi 1429 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓)) | |
2 | albii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1412 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1314 |
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 1408 ax-gen 1410 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2albii 1432 hbxfrbi 1433 nfbii 1434 19.26-2 1443 19.26-3an 1444 alrot3 1446 alrot4 1447 albiim 1448 2albiim 1449 alnex 1460 nfalt 1542 aaanh 1550 aaan 1551 alinexa 1567 exintrbi 1597 19.21-2 1630 19.31r 1644 equsalh 1689 equsal 1690 sbcof2 1766 dvelimfALT2 1773 19.23vv 1840 sbanv 1845 pm11.53 1851 nfsbxy 1895 nfsbxyt 1896 sbcomxyyz 1923 sb9 1932 sbnf2 1934 2sb6 1937 sbcom2v 1938 sb6a 1941 2sb6rf 1943 sbalyz 1952 sbal 1953 sbal1yz 1954 sbal1 1955 sbalv 1958 2exsb 1962 nfsb4t 1967 dvelimf 1968 dveeq1 1972 sbal2 1975 sb8eu 1990 sb8euh 2000 eu1 2002 eu2 2021 mo3h 2030 moanim 2051 2eu4 2070 exists1 2073 eqcom 2119 hblem 2225 abeq2 2226 abeq1 2227 nfceqi 2254 abid2f 2283 dfrex2dc 2405 ralbii2 2422 r2alf 2429 nfraldya 2446 r3al 2454 r19.21t 2484 r19.23t 2516 rabid2 2584 rabbi 2585 ralv 2677 ceqsralt 2687 gencbval 2708 rspc2gv 2775 ralab 2817 ralrab2 2822 euind 2844 reu2 2845 reu3 2847 rmo4 2850 reu8 2853 rmo3f 2854 rmoim 2858 2reuswapdc 2861 reuind 2862 2rmorex 2863 ra5 2969 rmo2ilem 2970 rmo3 2972 dfss2 3056 ss2ab 3135 ss2rab 3143 rabss 3144 uniiunlem 3155 dfdif3 3156 ddifstab 3178 ssequn1 3216 unss 3220 ralunb 3227 ssin 3268 ssddif 3280 n0rf 3345 eq0 3351 eqv 3352 rabeq0 3362 abeq0 3363 disj 3381 disj3 3385 rgenm 3435 pwss 3496 ralsnsg 3531 ralsns 3532 disjsn 3555 euabsn2 3562 snss 3619 snsssn 3658 dfnfc2 3724 uni0b 3731 unissb 3736 elintrab 3753 ssintrab 3764 intun 3772 intpr 3773 dfiin2g 3816 iunss 3824 dfdisj2 3878 cbvdisj 3886 disjnim 3890 dftr2 3998 dftr5 3999 trint 4011 zfnuleu 4022 vnex 4029 inex1 4032 repizf2lem 4055 axpweq 4065 zfpow 4069 axpow2 4070 axpow3 4071 exmid01 4091 zfpair2 4102 ssextss 4112 frirrg 4242 sucel 4302 zfun 4326 uniex2 4328 setindel 4423 setind 4424 elirr 4426 en2lp 4439 zfregfr 4458 tfi 4466 peano5 4482 ssrel 4597 ssrel2 4599 eqrelrel 4610 reliun 4630 raliunxp 4650 relop 4659 dmopab3 4722 dm0rn0 4726 reldm0 4727 cotr 4890 issref 4891 asymref 4894 intirr 4895 sb8iota 5065 dffun2 5103 dffun4 5104 dffun6f 5106 dffun4f 5109 dffun7 5120 funopab 5128 funcnv2 5153 funcnv 5154 funcnveq 5156 fun2cnv 5157 fun11 5160 fununi 5161 funcnvuni 5162 funimaexglem 5176 fnres 5209 fnopabg 5216 rexrnmpt 5531 dff13 5637 oprabidlem 5770 eqoprab2b 5797 mpo2eqb 5848 ralrnmpo 5853 dfer2 6398 fiintim 6785 ltexprlemdisj 7382 recexprlemdisj 7406 isprm2 11725 bj-stal 12884 bj-nfalt 12898 bdceq 12967 bdcriota 13008 bj-axempty2 13019 bj-vprc 13021 bdinex1 13024 bj-zfpair2 13035 bj-uniex2 13041 bj-ssom 13061 bj-inf2vnlem2 13096 ss1oel2o 13116 |
Copyright terms: Public domain | W3C validator |