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 476 | . 2 |
3 | 2 | adantll 473 | 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 5584 fiunsnnn 6855 addcomnqg 7330 addassnqg 7331 nqtri3or 7345 lt2addnq 7353 lt2mulnq 7354 enq0ref 7382 enq0tr 7383 nqnq0pi 7387 nqpnq0nq 7402 nqnq0a 7403 distrnq0 7408 addassnq0lemcl 7410 ltsrprg 7696 mulcomsrg 7706 mulasssrg 7707 distrsrg 7708 aptisr 7728 mulcnsr 7784 cnegex 8084 sub4 8151 muladd 8290 ltleadd 8352 divdivdivap 8617 divadddivap 8631 ltmul12a 8763 fzrev 10027 facndiv 10660 cncongr1 12044 blbas 13148 cncfmet 13294 ptolemy 13460 |
Copyright terms: Public domain | W3C validator |