Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad3antlr | Unicode version |
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
Ref | Expression |
---|---|
ad3antlr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 | |
2 | 1 | ad2antlr 458 | . 2 |
3 | 2 | adantr 261 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: ad4antlr 464 phpm 6327 phplem4on 6329 fidifsnen 6331 fisbth 6340 fin0 6342 fin0or 6343 prmuloc 6664 cauappcvgprlemopl 6744 cauappcvgprlemdisj 6749 cauappcvgprlemladdfl 6753 caucvgprlemopl 6767 axcaucvglemcau 6972 ssfzo12bi 9081 rebtwn2zlemstep 9107 btwnzge0 9142 cjap 9506 caucvgre 9580 |
Copyright terms: Public domain | W3C validator |