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 469 | . 2 |
3 | 2 | adantlr 468 | 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 5621 fcof1o 5683 infnfi 6782 addcomnqg 7182 addassnqg 7183 nqtri3or 7197 ltexnqq 7209 nqnq0pi 7239 nqpnq0nq 7254 nqnq0a 7255 addassnq0lemcl 7262 ltaddpr 7398 ltexprlemloc 7408 addcanprlemu 7416 recexprlem1ssu 7435 aptiprleml 7440 mulcomsrg 7558 mulasssrg 7559 distrsrg 7560 aptisr 7580 mulcnsr 7636 cnegex 7933 muladd 8139 lemul12b 8612 qaddcl 9420 iooshf 9728 elfzomelpfzo 10001 expnegzap 10320 setscom 11988 cnpnei 12377 |
Copyright terms: Public domain | W3C validator |