![]() |
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 494 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 276 |
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 |
This theorem is referenced by: ad6antr 498 difinfinf 7118 ctssdclemn0 7127 cauappcvgprlemladdfu 7671 caucvgprlemloc 7692 caucvgprlemladdfu 7694 caucvgprlemlim 7698 caucvgprprlemml 7711 caucvgprprlemloc 7720 caucvgprprlemlim 7728 suplocexprlemmu 7735 suplocexprlemru 7736 suplocexprlemloc 7738 suplocsrlem 7825 axcaucvglemres 7916 nn0ltexp2 10707 resqrexlemglsq 11049 xrmaxifle 11272 xrmaxiflemlub 11274 divalglemeuneg 11946 bezoutlemnewy 12015 ctiunctlemfo 12458 mhmmnd 13024 txmetcnp 14415 mulcncf 14488 suplociccreex 14499 cnplimclemr 14535 limccnpcntop 14541 lgsval 14802 |
Copyright terms: Public domain | W3C validator |