![]() |
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 13815 txlm 13864 metequiv2 14081 metcnpi3 14102 rescncf 14153 cncfco 14163 suplociccreex 14187 limcresi 14220 cnplimcim 14221 cnplimclemr 14223 cnlimcim 14225 limccnpcntop 14229 limccoap 14232 2sqlem6 14552 bj-charfunbi 14648 nninffeq 14854 tridceq 14889 |
Copyright terms: Public domain | W3C validator |