![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad4antr | Unicode version |
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad4antr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad3antrrr 476 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 270 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: ad5antr 480 tfr1onlemaccex 6045 tfrcllemaccex 6058 en2eqpr 6550 unsnfidcex 6557 unsnfidcel 6558 cauappcvgprlemloc 7114 caucvgprlemm 7130 caucvgprlemladdrl 7140 caucvgprlemlim 7143 caucvgprprlemml 7156 caucvgprprlemexbt 7168 caucvgprprlemlim 7173 caucvgsrlemgt1 7243 axcaucvglemres 7337 rebtwn2zlemstep 9553 hashunlem 10047 caucvgre 10241 cvg1nlemres 10245 resqrexlemglsq 10282 maxabslemval 10468 sumeq2d 10570 divalglemeunn 10701 dvdsbnd 10728 bezoutlemnewy 10765 bezoutlemmain 10767 |
Copyright terms: Public domain | W3C validator |