![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reximdva | Unicode version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
reximdva.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reximdva |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdva.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | reximdvai 2413 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 df-rex 2306 |
This theorem is referenced by: dffo4 5258 prarloclemarch 6401 appdivnq 6544 ltexprlemm 6574 ltexprlemopl 6575 ltexprlemopu 6577 ltexprlemloc 6581 archpr 6615 cauappcvgprlemm 6617 cauappcvgprlemopl 6618 cauappcvgprlemlol 6619 cauappcvgprlemopu 6620 cauappcvgprlemladdfu 6626 cauappcvgprlemladdfl 6627 caucvgprlemm 6639 caucvgprlemopl 6640 caucvgprlemlol 6641 caucvgprlemopu 6642 caucvgprlemladdfu 6648 caucvgprlemlim 6652 archsr 6708 cnegexlem2 6984 bndndx 7956 expnbnd 9025 expnlbnd2 9027 |
Copyright terms: Public domain | W3C validator |