![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad5antr | Unicode version |
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad5antr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad4antr 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: ad6antr 485 difinfinf 6901 ctssdclemn0 6910 cauappcvgprlemladdfu 7363 caucvgprlemloc 7384 caucvgprlemladdfu 7386 caucvgprlemlim 7390 caucvgprprlemml 7403 caucvgprprlemloc 7412 caucvgprprlemlim 7420 axcaucvglemres 7584 resqrexlemglsq 10634 xrmaxifle 10854 xrmaxiflemlub 10856 divalglemeuneg 11415 bezoutlemnewy 11477 mulcncf 12503 limccnpcntop 12520 |
Copyright terms: Public domain | W3C validator |