Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad2ant2lr | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 |
Ref | Expression |
---|---|
ad2ant2lr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 | |
2 | 1 | adantrr 470 | . 2 |
3 | 2 | adantll 467 | 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: mpteqb 5479 fiunsnnn 6743 addcomnqg 7157 addassnqg 7158 nqtri3or 7172 lt2addnq 7180 lt2mulnq 7181 enq0ref 7209 enq0tr 7210 nqnq0pi 7214 nqpnq0nq 7229 nqnq0a 7230 distrnq0 7235 addassnq0lemcl 7237 ltsrprg 7523 mulcomsrg 7533 mulasssrg 7534 distrsrg 7535 aptisr 7555 mulcnsr 7611 cnegex 7908 sub4 7975 muladd 8114 ltleadd 8176 divdivdivap 8441 divadddivap 8455 ltmul12a 8586 fzrev 9832 facndiv 10453 cncongr1 11711 blbas 12529 cncfmet 12675 ptolemy 12832 |
Copyright terms: Public domain | W3C validator |