Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad2ant2rl | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 |
Ref | Expression |
---|---|
ad2ant2rl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 | |
2 | 1 | adantrl 470 | . 2 |
3 | 2 | adantlr 469 | 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: fvtp1g 5687 fcof1o 5751 infnfi 6852 addcomnqg 7313 addassnqg 7314 nqtri3or 7328 ltexnqq 7340 nqnq0pi 7370 nqpnq0nq 7385 nqnq0a 7386 addassnq0lemcl 7393 ltaddpr 7529 ltexprlemloc 7539 addcanprlemu 7547 recexprlem1ssu 7566 aptiprleml 7571 mulcomsrg 7689 mulasssrg 7690 distrsrg 7691 aptisr 7711 mulcnsr 7767 cnegex 8067 muladd 8273 lemul12b 8747 qaddcl 9564 iooshf 9879 elfzomelpfzo 10156 expnegzap 10479 setscom 12377 cnpnei 12766 cxplt3 13387 cxple3 13388 |
Copyright terms: Public domain | W3C validator |