![]() |
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 481 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 272 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad5antr 485 tfr1onlemaccex 6199 tfrcllemaccex 6212 fimax2gtri 6748 en2eqpr 6754 unsnfidcex 6761 unsnfidcel 6762 ctssdc 6950 cauappcvgprlemloc 7408 caucvgprlemm 7424 caucvgprlemladdrl 7434 caucvgprlemlim 7437 caucvgprprlemml 7450 caucvgprprlemexbt 7462 caucvgprprlemlim 7467 caucvgsrlemgt1 7537 axcaucvglemres 7634 xaddval 9521 rebtwn2zlemstep 9923 hashunlem 10443 caucvgre 10645 cvg1nlemres 10649 resqrexlemglsq 10686 maxabslemval 10872 xrmaxiflemcl 10906 xrmaxifle 10907 xrmaxiflemab 10908 xrmaxiflemlub 10909 xrmaxiflemval 10911 xrmaxltsup 10919 divalglemeunn 11466 dvdsbnd 11493 bezoutlemnewy 11530 bezoutlemmain 11532 ctiunctlemfo 11795 txlm 12290 xmettx 12499 txmetcnp 12507 limcimo 12590 limccnp2cntop 12602 |
Copyright terms: Public domain | W3C validator |