![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimdva | Unicode version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
ralimdva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralimdva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1528 |
. 2
![]() ![]() ![]() ![]() | |
2 | ralimdva.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ralimdaa 2543 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 ax-4 1510 ax-17 1526 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 |
This theorem is referenced by: ralimdv 2545 ralimdvva 2546 f1mpt 5774 isores3 5818 caofrss 6109 caoftrn 6110 tfrlemibxssdm 6330 tfr1onlembxssdm 6346 tfrcllembxssdm 6359 tfrcl 6367 exmidomniim 7141 exmidontri2or 7244 caucvgsrlemoffcau 7799 caucvgsrlemoffres 7801 indstr 9595 caucvgre 10992 rexuz3 11001 resqrexlemgt0 11031 resqrexlemglsq 11033 cau3lem 11125 rexanre 11231 rexico 11232 2clim 11311 climcn1 11318 climcn2 11319 subcn2 11321 climsqz 11345 climsqz2 11346 climcvg1nlem 11359 fprodsplitdc 11606 bezoutlemaz 12006 bezoutlembz 12007 bezoutlembi 12008 pcfac 12350 pockthg 12357 infpnlem1 12359 isgrpinv 12931 dfgrp3me 12975 issubg4m 13058 cncnp 13769 txlm 13818 metequiv2 14035 metcnpi3 14056 rescncf 14107 cncfco 14117 suplociccreex 14141 limcresi 14174 cnplimcim 14175 cnplimclemr 14177 cnlimcim 14179 limccnpcntop 14183 limccoap 14186 2sqlem6 14506 bj-charfunbi 14602 nninffeq 14808 tridceq 14843 |
Copyright terms: Public domain | W3C validator |