![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimdv | Unicode version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.) |
Ref | Expression |
---|---|
ralimdv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralimdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 276 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralimdva 2544 |
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: poss 4298 sess1 4337 sess2 4338 riinint 4888 dffo4 5664 dffo5 5665 isoini2 5819 rdgivallem 6381 iinerm 6606 xpf1o 6843 exmidontriimlem3 7221 exmidontriim 7223 resqrexlemgt0 11028 cau3lem 11122 caubnd2 11125 climshftlemg 11309 climcau 11354 climcaucn 11358 serf0 11359 modfsummodlemstep 11464 bezoutlemmain 11998 ctinf 12430 strsetsid 12494 imasaddfnlemg 12734 fiinbas 13485 baspartn 13486 lmtopcnp 13686 rescncf 14004 limcresi 14071 |
Copyright terms: Public domain | W3C validator |