![]() |
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 1468 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓)) | |
2 | albii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1451 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ 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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 2albii 1471 hbxfrbi 1472 nfbii 1473 19.26-2 1482 19.26-3an 1483 alrot3 1485 alrot4 1486 albiim 1487 2albiim 1488 alnex 1499 nfalt 1578 aaanh 1586 aaan 1587 alinexa 1603 exintrbi 1633 19.21-2 1667 19.31r 1681 equsalh 1726 equsal 1727 equsalv 1793 sbcof2 1810 dvelimfALT2 1817 19.23vv 1884 sbanv 1889 pm11.53 1895 nfsbxy 1942 nfsbxyt 1943 sbcomxyyz 1972 sb9 1979 sbnf2 1981 2sb6 1984 sbcom2v 1985 sb6a 1988 2sb6rf 1990 sbalyz 1999 sbal 2000 sbal1yz 2001 sbal1 2002 sbalv 2005 2exsb 2009 nfsb4t 2014 dvelimf 2015 dveeq1 2019 sbal2 2020 sb8eu 2039 sb8euh 2049 eu1 2051 eu2 2070 mo3h 2079 moanim 2100 2eu4 2119 exists1 2122 eqcom 2179 hblem 2285 abeq2 2286 abeq1 2287 nfceqi 2315 abid2f 2345 dfrex2dc 2468 ralbii2 2487 r2alf 2494 nfraldya 2512 r3al 2521 r19.21t 2552 r19.23t 2584 rabid2 2654 rabbi 2655 ralv 2756 ceqsralt 2766 gencbval 2787 rspc2gv 2855 ralab 2899 ralrab2 2904 euind 2926 reu2 2927 reu3 2929 rmo4 2932 reu8 2935 rmo3f 2936 rmoim 2940 2reuswapdc 2943 reuind 2944 2rmorex 2945 ra5 3053 rmo2ilem 3054 rmo3 3056 dfss2 3146 ss2ab 3225 ss2rab 3233 rabss 3234 uniiunlem 3246 dfdif3 3247 ddifstab 3269 ssequn1 3307 unss 3311 ralunb 3318 ssin 3359 ssddif 3371 n0rf 3437 eq0 3443 eqv 3444 rabeq0 3454 abeq0 3455 disj 3473 disj3 3477 rgenm 3527 pwss 3593 ralsnsg 3631 ralsns 3632 disjsn 3656 euabsn2 3663 snssOLD 3720 snssb 3727 snsssn 3763 dfnfc2 3829 uni0b 3836 unissb 3841 elintrab 3858 ssintrab 3869 intun 3877 intpr 3878 dfiin2g 3921 iunss 3929 dfdisj2 3984 cbvdisj 3992 disjnim 3996 dftr2 4105 dftr5 4106 trint 4118 zfnuleu 4129 vnex 4136 inex1 4139 repizf2lem 4163 axpweq 4173 zfpow 4177 axpow2 4178 axpow3 4179 exmid01 4200 zfpair2 4212 ssextss 4222 frirrg 4352 sucel 4412 zfun 4436 uniex2 4438 setindel 4539 setind 4540 elirr 4542 en2lp 4555 zfregfr 4575 tfi 4583 peano5 4599 ssrel 4716 ssrel2 4718 eqrelrel 4729 reliun 4749 raliunxp 4770 relop 4779 dmopab3 4842 dm0rn0 4846 reldm0 4847 cotr 5012 issref 5013 asymref 5016 intirr 5017 sb8iota 5187 dffun2 5228 dffun4 5229 dffun6f 5231 dffun4f 5234 dffun7 5245 funopab 5253 funcnv2 5278 funcnv 5279 funcnveq 5281 fun2cnv 5282 fun11 5285 fununi 5286 funcnvuni 5287 funimaexglem 5301 fnres 5334 fnopabg 5341 rexrnmpt 5661 dff13 5771 oprabidlem 5908 eqoprab2b 5935 mpo2eqb 5986 ralrnmpo 5991 dfer2 6538 pw1dc0el 6913 fiintim 6930 omniwomnimkv 7167 ltexprlemdisj 7607 recexprlemdisj 7631 nnwosdc 12042 isprm2 12119 bj-stal 14586 bj-nfalt 14601 bdceq 14679 bdcriota 14720 bj-axempty2 14731 bj-vprc 14733 bdinex1 14736 bj-zfpair2 14747 bj-uniex2 14753 bj-ssom 14773 bj-inf2vnlem2 14808 ss1oel2o 14828 |
Copyright terms: Public domain | W3C validator |