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 491 | . 2 |
3 | 2 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad6antr 495 difinfinf 7074 ctssdclemn0 7083 cauappcvgprlemladdfu 7603 caucvgprlemloc 7624 caucvgprlemladdfu 7626 caucvgprlemlim 7630 caucvgprprlemml 7643 caucvgprprlemloc 7652 caucvgprprlemlim 7660 suplocexprlemmu 7667 suplocexprlemru 7668 suplocexprlemloc 7670 suplocsrlem 7757 axcaucvglemres 7848 nn0ltexp2 10631 resqrexlemglsq 10973 xrmaxifle 11196 xrmaxiflemlub 11198 divalglemeuneg 11869 bezoutlemnewy 11938 ctiunctlemfo 12381 txmetcnp 13271 mulcncf 13344 suplociccreex 13355 cnplimclemr 13391 limccnpcntop 13397 lgsval 13658 |
Copyright terms: Public domain | W3C validator |