![]() |
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 | ⊢ (∀xφ ↔ ∀xψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albi 1354 | . 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ)) | |
2 | albii.1 | . 2 ⊢ (φ ↔ ψ) | |
3 | 1, 2 | mpg 1337 | 1 ⊢ (∀xφ ↔ ∀xψ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1240 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 2albii 1357 hbxfrbi 1358 nfbii 1359 19.26-2 1368 19.26-3an 1369 alrot3 1371 alrot4 1372 albiim 1373 2albiim 1374 alnex 1385 nfalt 1467 aaanh 1475 aaan 1476 alinexa 1491 exintrbi 1521 19.21-2 1554 19.31r 1568 equsalh 1611 equsal 1612 sbcof2 1688 dvelimfALT2 1695 19.23vv 1761 sbanv 1766 pm11.53 1772 nfsbxy 1815 nfsbxyt 1816 sbcomxyyz 1843 sb9 1852 sbnf2 1854 2sb6 1857 sbcom2v 1858 sb6a 1861 2sb6rf 1863 sbalyz 1872 sbal 1873 sbal1yz 1874 sbal1 1875 sbalv 1878 2exsb 1882 nfsb4t 1887 dvelimf 1888 dveeq1 1892 sbal2 1895 sb8eu 1910 sb8euh 1920 eu1 1922 eu2 1941 mo3h 1950 moanim 1971 2eu4 1990 exists1 1993 eqcom 2039 hblem 2142 abeq2 2143 abeq1 2144 nfceqi 2171 abid2f 2199 ralbii2 2328 r2alf 2335 nfraldya 2352 r3al 2360 r19.21t 2388 r19.23t 2417 rabid2 2480 rabbi 2481 ralv 2565 ceqsralt 2575 gencbval 2596 ralab 2695 ralrab2 2700 euind 2722 reu2 2723 reu3 2725 rmo4 2728 reu8 2731 rmoim 2734 2reuswapdc 2737 reuind 2738 2rmorex 2739 ra5 2840 rmo2ilem 2841 rmo3 2843 dfss2 2928 ss2ab 3002 ss2rab 3010 rabss 3011 uniiunlem 3022 ssequn1 3107 unss 3111 ralunb 3118 ssin 3153 ssddif 3165 n0rf 3227 eq0 3233 eqv 3234 rabeq0 3241 abeq0 3242 disj 3262 disj3 3266 rgenm 3317 pwss 3366 ralsns 3399 disjsn 3423 euabsn2 3430 snss 3485 snsssn 3523 dfnfc2 3589 uni0b 3596 unissb 3601 elintrab 3618 ssintrab 3629 intun 3637 intpr 3638 dfiin2g 3681 iunss 3689 dfdisj2 3738 cbvdisj 3746 dftr2 3847 dftr5 3848 trint 3860 zfnuleu 3872 vprc 3879 inex1 3882 repizf2lem 3905 axpweq 3915 zfpow 3919 axpow2 3920 axpow3 3921 zfpair2 3936 ssextss 3947 sucel 4113 zfun 4137 uniex2 4139 setindel 4221 setind 4222 elirr 4224 en2lp 4232 tfi 4248 peano5 4264 ssrel 4371 ssrel2 4373 eqrelrel 4384 reliun 4401 raliunxp 4420 relop 4429 dmopab3 4491 dm0rn0 4495 reldm0 4496 cotr 4649 issref 4650 asymref 4653 intirr 4654 sb8iota 4817 dffun2 4855 dffun4 4856 dffun6f 4858 dffun4f 4861 dffun7 4871 funopab 4878 funcnv2 4902 funcnv 4903 funcnveq 4905 fun2cnv 4906 fun11 4909 fununi 4910 funcnvuni 4911 funimaexglem 4925 fnres 4958 fnopabg 4965 rexrnmpt 5253 dff13 5350 oprabidlem 5479 eqoprab2b 5505 mpt22eqb 5552 ralrnmpt2 5557 dfer2 6043 ltexprlemdisj 6580 recexprlemdisj 6602 bj-nfalt 9239 bdceq 9297 bdcriota 9338 bj-axempty2 9349 bj-vprc 9351 bdinex1 9354 bj-zfpair2 9365 bj-uniex2 9371 bj-ssom 9395 peano5setOLD 9400 bj-inf2vnlem2 9431 |
Copyright terms: Public domain | W3C validator |