![]() |
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 1425 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓)) | |
2 | albii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1408 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1310 |
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 1404 ax-gen 1406 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2albii 1428 hbxfrbi 1429 nfbii 1430 19.26-2 1439 19.26-3an 1440 alrot3 1442 alrot4 1443 albiim 1444 2albiim 1445 alnex 1456 nfalt 1538 aaanh 1546 aaan 1547 alinexa 1563 exintrbi 1593 19.21-2 1626 19.31r 1640 equsalh 1685 equsal 1686 sbcof2 1762 dvelimfALT2 1769 19.23vv 1836 sbanv 1841 pm11.53 1847 nfsbxy 1891 nfsbxyt 1892 sbcomxyyz 1919 sb9 1928 sbnf2 1930 2sb6 1933 sbcom2v 1934 sb6a 1937 2sb6rf 1939 sbalyz 1948 sbal 1949 sbal1yz 1950 sbal1 1951 sbalv 1954 2exsb 1958 nfsb4t 1963 dvelimf 1964 dveeq1 1968 sbal2 1971 sb8eu 1986 sb8euh 1996 eu1 1998 eu2 2017 mo3h 2026 moanim 2047 2eu4 2066 exists1 2069 eqcom 2115 hblem 2220 abeq2 2221 abeq1 2222 nfceqi 2249 abid2f 2278 dfrex2dc 2400 ralbii2 2417 r2alf 2424 nfraldya 2441 r3al 2449 r19.21t 2479 r19.23t 2511 rabid2 2579 rabbi 2580 ralv 2672 ceqsralt 2682 gencbval 2703 rspc2gv 2769 ralab 2811 ralrab2 2816 euind 2838 reu2 2839 reu3 2841 rmo4 2844 reu8 2847 rmo3f 2848 rmoim 2852 2reuswapdc 2855 reuind 2856 2rmorex 2857 ra5 2963 rmo2ilem 2964 rmo3 2966 dfss2 3050 ss2ab 3129 ss2rab 3137 rabss 3138 uniiunlem 3149 dfdif3 3150 ddifstab 3172 ssequn1 3210 unss 3214 ralunb 3221 ssin 3262 ssddif 3274 n0rf 3339 eq0 3345 eqv 3346 rabeq0 3356 abeq0 3357 disj 3375 disj3 3379 rgenm 3429 pwss 3490 ralsnsg 3525 ralsns 3526 disjsn 3549 euabsn2 3556 snss 3613 snsssn 3652 dfnfc2 3718 uni0b 3725 unissb 3730 elintrab 3747 ssintrab 3758 intun 3766 intpr 3767 dfiin2g 3810 iunss 3818 dfdisj2 3872 cbvdisj 3880 disjnim 3884 dftr2 3986 dftr5 3987 trint 3999 zfnuleu 4010 vnex 4017 inex1 4020 repizf2lem 4043 axpweq 4053 zfpow 4057 axpow2 4058 axpow3 4059 exmid01 4079 zfpair2 4090 ssextss 4100 frirrg 4230 sucel 4290 zfun 4314 uniex2 4316 setindel 4411 setind 4412 elirr 4414 en2lp 4427 zfregfr 4446 tfi 4454 peano5 4470 ssrel 4585 ssrel2 4587 eqrelrel 4598 reliun 4618 raliunxp 4638 relop 4647 dmopab3 4710 dm0rn0 4714 reldm0 4715 cotr 4876 issref 4877 asymref 4880 intirr 4881 sb8iota 5051 dffun2 5089 dffun4 5090 dffun6f 5092 dffun4f 5095 dffun7 5106 funopab 5114 funcnv2 5139 funcnv 5140 funcnveq 5142 fun2cnv 5143 fun11 5146 fununi 5147 funcnvuni 5148 funimaexglem 5162 fnres 5195 fnopabg 5202 rexrnmpt 5515 dff13 5621 oprabidlem 5754 eqoprab2b 5781 mpo2eqb 5832 ralrnmpo 5837 dfer2 6381 fiintim 6767 ltexprlemdisj 7355 recexprlemdisj 7379 isprm2 11637 bj-stal 12636 bj-nfalt 12651 bdceq 12719 bdcriota 12760 bj-axempty2 12771 bj-vprc 12773 bdinex1 12776 bj-zfpair2 12787 bj-uniex2 12793 bj-ssom 12813 bj-inf2vnlem2 12848 ss1oel2o 12868 |
Copyright terms: Public domain | W3C validator |