![]() |
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 471 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantll 468 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 5519 fiunsnnn 6783 addcomnqg 7213 addassnqg 7214 nqtri3or 7228 lt2addnq 7236 lt2mulnq 7237 enq0ref 7265 enq0tr 7266 nqnq0pi 7270 nqpnq0nq 7285 nqnq0a 7286 distrnq0 7291 addassnq0lemcl 7293 ltsrprg 7579 mulcomsrg 7589 mulasssrg 7590 distrsrg 7591 aptisr 7611 mulcnsr 7667 cnegex 7964 sub4 8031 muladd 8170 ltleadd 8232 divdivdivap 8497 divadddivap 8511 ltmul12a 8642 fzrev 9895 facndiv 10517 cncongr1 11820 blbas 12641 cncfmet 12787 ptolemy 12953 |
Copyright terms: Public domain | W3C validator |